---

Step * of Lemma callbyvalueall-single-append-nil

∀[F,a:Top].  (let x ⟵ [a] in let y ⟵ x @ [] in F[y] ~ let y ⟵ [a] in F[y])
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "callbyvalueall-single" 0 THENA Auto)
   THEN SqEqualTopToBase
   THEN UseCbvaSq
   THEN RepUR ``append`` 0
   THEN CallByValueReduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,a:Top].    (let  x  \mleftarrow{}{}  [a]  in  let  y  \mleftarrow{}{}  x  @  []  in  F[y]  \msim{}  let  y  \mleftarrow{}{}  [a]  in  F[y])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "callbyvalueall-single"  0  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  UseCbvaSq
  THEN  RepUR  ``append``  0
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index