---

Step * of Lemma lifting-apply-less

∀[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