Step * of Lemma constant-cubical-type-at

[X,I,a:Top].  ((X)(a) X(I))
BY
(Auto THEN RepUR ``constant-cubical-type cubical-type-at`` THEN Auto) }


Latex:


Latex:
\mforall{}[X,I,a:Top].    ((X)(a)  \msim{}  X(I))


By


Latex:
(Auto  THEN  RepUR  ``constant-cubical-type  cubical-type-at``  0  THEN  Auto)




Home Index