---

Step * of Lemma has-value-is-list-map-iff-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) THEN RepeatFor 2 (Intro) THEN (Assert (is-list(t))↓ ∈ ℙ BY Auto) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((RWO  "is-list-map"  0  THENA  Auto)
  THEN  RepeatFor  2  (Intro)
  THEN  (Assert  (is-list(t))\mdownarrow{}  \mmember{}  \mBbbP{}  BY
                          Auto)
  THEN  Auto)

---

Home Index