---

Step * of Lemma lifting-callbyvalueall-spread

∀[p,F,G:Top].  (let x ⟵ let a,b = p in F[a;b] in G[x] ~ let a,b = p in let x ⟵ F[a;b] in G[x])
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[p,F,G:Top].    (let  x  \mleftarrow{}{}  let  a,b  =  p  in  F[a;b]  in  G[x]  \msim{}  let  a,b  =  p  in  let  x  \mleftarrow{}{}  F[a;b]  in  G[x])


By

---

Latex:
ProveLiftingLemma

---

Home Index