Step * of Lemma fl_all-1

I,J,i:Top.  ((∀i.1) 1)
BY
(Auto THEN RepeatFor ((RW (SubC (TagC (mk_tag_term 10000))) 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