---

Step * of Lemma nil-sub-co-list

∀[T:Type]. ∀[s:colist(T)].  sub-co-list(T;[];s)
BY
{ (Auto THEN (Assert [] ∈ colist(ℕ) BY (SubsumeC ⌜ℕ List⌝⋅ THEN Auto)) THEN (D 0 With ⌜[]⌝  THENA Auto)) }

1
1. T : Type
2. s : colist(T)
3. [] ∈ colist(ℕ)
⊢ [] = s@[] ∈ colist(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:colist(T)].    sub-co-list(T;[];s)


By

---

Latex:
(Auto
  THEN  (Assert  []  \mmember{}  colist(\mBbbN{})  BY
                          (SubsumeC  \mkleeneopen{}\mBbbN{}  List\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}[]\mkleeneclose{}    THENA  Auto))

---

Home Index