Step * of Lemma co-list-islist-islist-new-compactness-base

[T:Type]. ∀[t:co-list-islist(T)].  islist(t)
BY
(Auto THEN Unfold `islist` THEN UseWitness ⌜Ax⌝⋅}


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[t:co-list-islist(T)].    islist(t)


By


Latex:
(Auto  THEN  Unfold  `islist`  0  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{})




Home Index