---

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


∀[T:Type]. ∀[t:colist(T)]. ∀[f:Base].  ((is-list(t))↓ ⇒ (is-list(t))↓)
BY
{ (RepeatFor 3 (Intro) THEN At ⌜Type⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  3  (Intro)  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index