---

Step * of Lemma last-not-before

∀[T:Type]. ∀L:T List. (∀x:T. (last(L) before x ∈ L ⇐⇒ False)) supposing (no_repeats(T;L) and (¬↑null(L)))
BY
{ (Auto
   THEN ((InstLemma `no_repeats_iff` [⌜T⌝; ⌜L⌝])⋅ THENA Auto)
   THEN ThinTrivial
   THEN ((FHyp (-1) [-2]) THENA Auto)
   THEN InstLemma `before_last` [⌜T⌝;⌜L⌝;⌜x⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. L : T List
3. ¬↑null(L)
4. no_repeats(T;L)
5. x : T
6. last(L) before x ∈ L
7. ∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ L
8. ¬(last(L) = x ∈ T)
⊢ (x ∈ L)

2
1. T : Type
2. L : T List
3. ¬↑null(L)
4. no_repeats(T;L)
5. x : T
6. last(L) before x ∈ L
7. ∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ L
8. ¬(last(L) = x ∈ T)
9. x before last(L) ∈ L
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  (\mforall{}x:T.  (last(L)  before  x  \mmember{}  L  \mLeftarrow{}{}\mRightarrow{}  False))  supposing  (no\_repeats(T;L)  and  (\mneg{}\muparrow{}null(L)))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `no\_repeats\_iff`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ThinTrivial
  THEN  ((FHyp  (-1)  [-2])  THENA  Auto)
  THEN  InstLemma  `before\_last`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index