---

Step * of Lemma co-list-islist-induction1

∀[A:Type]. ∀[P:co-list-islist(A) ⟶ ℙ].
  (P[conil()] ⇒ (∀L:co-list-islist(A). ∀a:A.  (P[L] ⇒ P[cocons(a;L)])) ⇒ (∀L:co-list-islist(A). P[L]))
BY
{ (UnivCD THENA Auto) }

1
1. [A] : Type
2. [P] : co-list-islist(A) ⟶ ℙ
3. P[conil()]@i
4. ∀L:co-list-islist(A). ∀a:A.  (P[L] ⇒ P[cocons(a;L)])@i
5. L : co-list-islist(A)@i
⊢ P[L]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:co-list-islist(A)  {}\mrightarrow{}  \mBbbP{}].
    (P[conil()]
    {}\mRightarrow{}  (\mforall{}L:co-list-islist(A).  \mforall{}a:A.    (P[L]  {}\mRightarrow{}  P[cocons(a;L)]))
    {}\mRightarrow{}  (\mforall{}L:co-list-islist(A).  P[L]))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index