---

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

∀[T:Type]. ∀[t:colist(T)]. ∀[f:Base].  ((is-list(t))↓ ⇒ (is-list(map(f;t)))↓)
BY
{ (RWO "is-list-map" 0 THENA Auto) }

1
∀[T:Type]. ∀[t:colist(T)]. ∀[f:Base].  ((is-list(t))↓ ⇒ (is-list(t))↓)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].  \mforall{}[f:Base].    ((is-list(t))\mdownarrow{}  {}\mRightarrow{}  (is-list(map(f;t)))\mdownarrow{})


By

---

Latex:
(RWO  "is-list-map"  0  THENA  Auto)

---

Home Index