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