---

Step * 1 of Lemma l-last-is-last


1. l : Base
2. ∀l:Top List. (l-last(l) ~ last(l))
3. is-exception(l-last(l))
⊢ l-last(l) ≤ last(l)
BY
{ (ExceptionSqequal (-1)
   THEN HypSubst' (-1) 0
   THEN (Assert exception(u; v) ≤ l-last(l) BY
               (HypSubst' (-1) 0 THEN Auto))
   THEN Lemmaize [-1]
   THEN (UnivCD THENA Auto)) }

1
1. l : Base@i
2. u : Base@i
3. v : Base@i
4. exception(u; v) ≤ l-last(l)
⊢ exception(u; v) ≤ last(l)

---

Latex:

---

Latex:

1.  l  :  Base
2.  \mforall{}l:Top  List.  (l-last(l)  \msim{}  last(l))
3.  is-exception(l-last(l))
\mvdash{}  l-last(l)  \mleq{}  last(l)


By

---

Latex:
(ExceptionSqequal  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  (Assert  exception(u;  v)  \mleq{}  l-last(l)  BY
                          (HypSubst'  (-1)  0  THEN  Auto))
  THEN  Lemmaize  [-1]
  THEN  (UnivCD  THENA  Auto))

---

Home Index