---

Step * of Lemma l_before_select

∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||.  L[j] before L[i] ∈ L supposing j < i
BY
{ ((Unfold `l_before` 0 THEN Auto{1,3}-1) THEN Easy) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i,j:\mBbbN{}||L||.    L[j]  before  L[i]  \mmember{}  L  supposing  j  <  i


By

---

Latex:
((Unfold  `l\_before`  0  THEN  Auto\{1,3\}-1)  THEN  Easy)

---

Home Index