---

Step * of Lemma lifting-apply-callbyvalueall

∀[a,B,c:Top].  (let x ⟵ a in B[x] c ~ let x ⟵ a in B[x] c)
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,B,c:Top].    (let  x  \mleftarrow{}{}  a  in  B[x]  c  \msim{}  let  x  \mleftarrow{}{}  a  in  B[x]  c)


By

---

Latex:
ProveLiftingLemma

---

Home Index