---

Step * of Lemma callbyvalueall-single-repeat

∀[F,a:Top].  (let x ⟵ [a] in let y ⟵ x in F[y] ~ let x ⟵ [a] in F[x])
BY
{ ((UnivCD THENA Auto)
   THEN (RWO  "callbyvalueall-single" 0 THENA Auto)
   THEN SqEqualTopToBase
   THEN UseCbvaSq
   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  x  \mleftarrow{}{}  [a]  in  F[x])


By

---

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

---

Home Index