---

Step * of Lemma before-hd

∀[T:Type]. ∀L:T List. (∀x:T. (x before hd(L) ∈ L ⇐⇒ False)) supposing (no_repeats(T;L) and 0 < ||L||)
BY
{ (Auto THEN (((InstLemma `no_repeats_iff` [⌜T⌝; ⌜L⌝])⋅ THENM ThinTrivial) THENA Auto)) }

1
1. T : Type
2. L : T List
3. 0 < ||L||
4. no_repeats(T;L)
5. x : T
6. x before hd(L) ∈ L
7. ∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ L
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  (\mforall{}x:T.  (x  before  hd(L)  \mmember{}  L  \mLeftarrow{}{}\mRightarrow{}  False))  supposing  (no\_repeats(T;L)  and  0  <  ||L||)


By

---

Latex:
(Auto  THEN  (((InstLemma  `no\_repeats\_iff`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THENM  ThinTrivial)  THENA  Auto))

---

Home Index