---

Step * of Lemma lifting-add-isaxiom-2

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

---

Latex:

---

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


By

---

Latex:
SqReasoning

---

Home Index