---

Step * of Lemma fl_all-1

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

---

Latex:

---

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


By

---

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

---

Home Index