---

Step * of Lemma single_iseg

∀[T:Type]. ∀L:T List. ∀x:T.  ([x] ≤ L ⇐⇒ 0 < ||L|| ∧ (L[0] = x ∈ T))
BY
{ ((UnivCD THENA Auto) THEN DVar `L'⋅) }

1
1. [T] : Type
2. x : T
⊢ [x] ≤ [] ⇐⇒ 0 < ||[]|| ∧ ([][0] = x ∈ T)

2
1. [T] : Type
2. u : T
3. v : T List
4. x : T
⊢ [x] ≤ [u / v] ⇐⇒ 0 < ||[u / v]|| ∧ ([u / v][0] = x ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    ([x]  \mleq{}  L  \mLeftarrow{}{}\mRightarrow{}  0  <  ||L||  \mwedge{}  (L[0]  =  x))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  DVar  `L'\mcdot{})

---

Home Index