---

Step * of Lemma lifting-add-ispair-2

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

---

Latex:

---

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


By

---

Latex:
SqReasoning

---

Home Index