---

Step * 1 of Lemma iseg_select


1. [T] : Type
⊢ ∀l2:T List. ([] ≤ l2 ⇐⇒ (||[]|| ≤ ||l2||) c∧ (∀i:ℕ. [][i] = l2[i] ∈ T supposing i < ||[]||))
BY
{ TACTIC:(Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}l2:T  List.  ([]  \mleq{}  l2  \mLeftarrow{}{}\mRightarrow{}  (||[]||  \mleq{}  ||l2||)  c\mwedge{}  (\mforall{}i:\mBbbN{}.  [][i]  =  l2[i]  supposing  i  <  ||[]||))


By

---

Latex:
TACTIC:(Reduce  0  THEN  Auto)

---

Home Index