---

Step * of Lemma last-map

∀[as:Top List]. ∀[f:Top].  last(map(f;as)) ~ f last(as) supposing ¬↑null(as)
BY
{ TACTIC:((((UnivCD THENA Auto) THEN Unfold `last` 0 THEN RWO "length-map" 0) THENA Auto)
          THEN RWO "select-map" 0
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[as:Top  List].  \mforall{}[f:Top].    last(map(f;as))  \msim{}  f  last(as)  supposing  \mneg{}\muparrow{}null(as)


By

---

Latex:
TACTIC:((((UnivCD  THENA  Auto)  THEN  Unfold  `last`  0  THEN  RWO  "length-map"  0)  THENA  Auto)
                THEN  RWO  "select-map"  0
                THEN  Auto)

---

Home Index