---

Step * of Lemma nil-contains

∀[T:Type]. ∀L:T List. (L ⊆ [] ⇐⇒ ↑null(L))
BY
{ ((UnivCD THENA Auto) THEN D -1 THEN Reduce 0) }

1
1. [T] : Type
⊢ [] ⊆ [] ⇐⇒ True

2
1. [T] : Type
2. u : T
3. v : T List
⊢ [u / v] ⊆ [] ⇐⇒ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  (L  \msubseteq{}  []  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}null(L))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -1  THEN  Reduce  0)

---

Home Index