---

Step * of Lemma lifting-add-isaxiom-1

∀[a,b,c,d:Top].  (if b = Ax then c otherwise d + a ~ if b = Ax then c + a otherwise d + a)
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:Top].    (if  b  =  Ax  then  c  otherwise  d  +  a  \msim{}  if  b  =  Ax  then  c  +  a  otherwise  d  +  a)


By

---

Latex:
ProveLiftingLemma

---

Home Index