---

Step * of Lemma fl_all-0

∀I,J,i:Top.  ((∀i.0) ~ 0)
BY
{ (Auto THEN RW (SubC (TagC (mk_tag_term 10000))) 0 THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}I,J,i:Top.    ((\mforall{}i.0)  \msim{}  0)


By

---

Latex:
(Auto  THEN  RW  (SubC  (TagC  (mk\_tag\_term  10000)))  0  THEN  EqCD)

---

Home Index