---

Step * of Lemma lifting-apply-int_eq

∀[n,m,a,b,c:Top].  (if n=m  then a  else b c ~ if n=m  then a c  else (b c))
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[n,m,a,b,c:Top].    (if  n=m    then  a    else  b  c  \msim{}  if  n=m    then  a  c    else  (b  c))


By

---

Latex:
ProveLiftingLemma

---

Home Index