Step
*
of Lemma
co-list-cons_wf
∀[T:Type]. ∀[h:T]. ∀[t:colist(T)]. (co-list-cons(h;t) ∈ colist(T))
BY
{ (ProveWfLemma THEN SubsumeC ⌜Unit ⋃ (T × colist(T))⌝⋅ THEN Auto) }
1
1. T : Type
2. h : T
3. t : colist(T)
4. <h, t> = <h, t> ∈ (Unit ⋃ (T × colist(T)))
⊢ (Unit ⋃ (T × colist(T))) ⊆r colist(T)
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[h:T]. \mforall{}[t:colist(T)]. (co-list-cons(h;t) \mmember{} colist(T))
By
Latex:
(ProveWfLemma THEN SubsumeC \mkleeneopen{}Unit \mcup{} (T \mtimes{} colist(T))\mkleeneclose{}\mcdot{} THEN Auto)
Home
Index