---

Step * of Lemma l_subset_nil_right

∀[T:Type]. ∀[L:T List].  (l_subset(T;L;[]) ⇐⇒ L = [] ∈ (T List))
BY
{ (RepUR ``l_subset`` 0 THEN Auto THEN Try ((GenListD (-1)⋅ THEN Auto))) }

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

---

Latex:

---

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


By

---

Latex:
(RepUR  ``l\_subset``  0  THEN  Auto  THEN  Try  ((GenListD  (-1)\mcdot{}  THEN  Auto)))

---

Home Index