---

Step * of Lemma has-value-if-has-value-map

∀[t,f:Base].  (t)↓ supposing (map(f;t))↓
BY
{ (Auto THEN RepUR ``map`` (-1) THEN RecUnfold `list_ind` (-1) THEN HasValueD (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[t,f:Base].    (t)\mdownarrow{}  supposing  (map(f;t))\mdownarrow{}


By

---

Latex:
(Auto  THEN  RepUR  ``map``  (-1)  THEN  RecUnfold  `list\_ind`  (-1)  THEN  HasValueD  (-1)  THEN  Trivial)

---

Home Index