---

Step * of Lemma hd-before

∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ hd(L) before x ∈ L supposing ¬(x = hd(L) ∈ T)) supposing 0 < ||L||
BY
{ (Auto THEN DVar `L' THEN All Reduce THEN Auto') }

1
1. [T] : Type
2. u : T
3. v : T List
4. 0 < ||v|| + 1
5. x : T
6. (x ∈ [u / v])
7. ¬(x = u ∈ T)
⊢ u before x ∈ [u / v]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}x:T.  ((x  \mmember{}  L)  {}\mRightarrow{}  hd(L)  before  x  \mmember{}  L  supposing  \mneg{}(x  =  hd(L)))  supposing  0  <  ||L||


By

---

Latex:
(Auto  THEN  DVar  `L'  THEN  All  Reduce  THEN  Auto')

---

Home Index