---

Step * of Lemma lifting-apply-callbyvalue

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

---

Latex:

---

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


By

---

Latex:
ProveLiftingLemma

---

Home Index