Step * of Lemma dM1-sq-1

[I:Top]. (1 1)
BY
(Auto THEN RW (SubC (SymbCompC [] 100)) THEN Auto) }


Latex:


Latex:
\mforall{}[I:Top].  (1  \msim{}  1)


By


Latex:
(Auto  THEN  RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto)




Home Index