---

Step * of Lemma sublist_nil

∀[T:Type]. ∀L:T List. (L ⊆ [] ⇐⇒ L = [] ∈ (T List))
BY
{ Auto }

1
1. T : Type
2. L : T List
3. L ⊆ []
⊢ L = [] ∈ (T List)

2
1. [T] : Type
2. L : T List
3. L = [] ∈ (T List)
⊢ L ⊆ []

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index