---

Step * of Lemma last-cons

∀[x:Top]. ∀[as:Top List].  (last([x / as]) ~ if null(as) then x else last(as) fi )
BY
{ ((UnivCD THENA Auto) THEN Unfold `last` 0 THEN (D (-1)) THEN Reduce 0 THEN Try (Trivial)) }

1
1. x : Top
2. u : Top
3. v : Top List
⊢ [x; [u / v]][((||v|| + 1) + 1) - 1] ~ [u / v][(||v|| + 1) - 1]

---

Latex:

---

Latex:
\mforall{}[x:Top].  \mforall{}[as:Top  List].    (last([x  /  as])  \msim{}  if  null(as)  then  x  else  last(as)  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `last`  0  THEN  (D  (-1))  THEN  Reduce  0  THEN  Try  (Trivial))

---

Home Index