Step
*
of Lemma
co-list-nil_wf
∀[T:Type]. (co-list-nil() ∈ colist(T))
BY
{ (ProveWfLemma THEN Fold `it` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type].  (co-list-nil()  \mmember{}  colist(T))
By
Latex:
(ProveWfLemma  THEN  Fold  `it`  0  THEN  Auto)
Home
Index