---

Step * 1 of Lemma before-hd


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
BY
{ ((FHyp (-1) [-2] THENA Auto)⋅
   THEN (InstLemma `hd-before` [⌜T⌝;⌜L⌝;⌜x⌝]⋅ THENA (Auto THEN (FLemma `l_before_member2` [-3] THEN 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
8. ¬(x = hd(L) ∈ T)
9. hd(L) before x ∈ L
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  0  <  ||L||
4.  no\_repeats(T;L)
5.  x  :  T
6.  x  before  hd(L)  \mmember{}  L
7.  \mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  x  before  y  \mmember{}  L
\mvdash{}  False


By

---

Latex:
((FHyp  (-1)  [-2]  THENA  Auto)\mcdot{}
  THEN  (InstLemma  `hd-before`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  (FLemma  `l\_before\_member2`  [-3]  THEN  Auto)\mcdot{})
              )
  )

---

Home Index