Step * of Lemma trivial-cube-set_wf

() ∈ CubicalSet
BY
(Unfold `trivial-cube-set` THEN MemTypeCD THEN Reduce THEN Auto) }


Latex:


Latex:
()  \mmember{}  CubicalSet


By


Latex:
(Unfold  `trivial-cube-set`  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)




Home Index