---

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

∀[T:Type]. ∀x:T. ∀L:colist(T).  (sub-co-list(T;[x / L];[]) ⇐⇒ False)
BY
{ (UnivCD THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}L:colist(T).    (sub-co-list(T;[x  /  L];[])  \mLeftarrow{}{}\mRightarrow{}  False)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index