---

Step * of Lemma lifting-add-ispair-1

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

---

Latex:

---

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


By

---

Latex:
ProveLiftingLemma

---

Home Index