---

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


1. [T] : Type
2. x : T
3. L : colist(T)
⊢ sub-co-list(T;[x / L];[]) ⇐⇒ False
BY
{ D 0 }

1
1. [T] : Type
2. x : T
3. L : colist(T)
⊢ sub-co-list(T;[x / L];[]) ⇒ False

2
1. [T] : Type
2. x : T
3. L : colist(T)
⊢ sub-co-list(T;[x / L];[]) ⇐ False

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T
3.  L  :  colist(T)
\mvdash{}  sub-co-list(T;[x  /  L];[])  \mLeftarrow{}{}\mRightarrow{}  False


By

---

Latex:
D  0

---

Home Index