---

Step * of Lemma dM-lift-1-sq

∀[I,J,f:Top].  (dM-lift(I;J;f) 1 ~ 1)
BY
{ (Auto THEN RepeatFor 2 ((RW (SubC (TagC (mk_tag_term 2000))) 0 THEN EqCD))) }

---

Latex:

---

Latex:
\mforall{}[I,J,f:Top].    (dM-lift(I;J;f)  1  \msim{}  1)


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((RW  (SubC  (TagC  (mk\_tag\_term  2000)))  0  THEN  EqCD)))

---

Home Index