---

Step * of Lemma lifting-apply-atom_eq

∀[n,m,a,b,c:Top].  (if n=m then a else b fi  c ~ if n=m then a c else b c fi )
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[n,m,a,b,c:Top].    (if  n=m  then  a  else  b  fi    c  \msim{}  if  n=m  then  a  c  else  b  c  fi  )


By

---

Latex:
ProveLiftingLemma

---

Home Index