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