---

Step * 1 1 1 1 1 1 of Lemma cons-sub-co-list-nil

.....fun wf..... 
1. T : Type
2. x : T
3. L : colist(T)
4. ns : colist(ℕ)
5. [x / L] = [] ∈ colist(T)
6. Z : colist(T)
⊢ null(Z) = null(Z)
BY
{ Thin (-2) }

1
1. T : Type
2. x : T
3. L : colist(T)
4. ns : colist(ℕ)
5. Z : colist(T)
⊢ null(Z) = null(Z)

---

Latex:

---

Latex:
.....fun  wf..... 
1.  T  :  Type
2.  x  :  T
3.  L  :  colist(T)
4.  ns  :  colist(\mBbbN{})
5.  [x  /  L]  =  []
6.  Z  :  colist(T)
\mvdash{}  null(Z)  =  null(Z)


By

---

Latex:
Thin  (-2)

---

Home Index