---

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


1. [T] : Type
2. x : T
3. L : colist(T)
4. ns : colist(ℕ)
5. [x / L] = [] ∈ colist(T)
⊢ False
BY
{ ApFunToHypEquands `Z' ⌜null(Z)⌝ ⌜𝔹⌝ (-1)⋅ }

1
.....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)

2
1. [T] : Type
2. x : T
3. L : colist(T)
4. ns : colist(ℕ)
5. [x / L] = [] ∈ colist(T)
6. null([x / L]) = null([])
⊢ False

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T
3.  L  :  colist(T)
4.  ns  :  colist(\mBbbN{})
5.  [x  /  L]  =  []
\mvdash{}  False


By

---

Latex:
ApFunToHypEquands  `Z'  \mkleeneopen{}null(Z)\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}

---

Home Index