---

Step * of Lemma callbyvalueall-reduce-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 SqEqualBase THEN UseCbvaSq) }

1
1. F : Base
2. a : Base
3. has-valueall(a)@i
⊢ let y ⟵ evalall(a)
  in F[y] ~ F[evalall(a)]

---

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  SqEqualBase  THEN  UseCbvaSq)

---

Home Index