---

Step * of Lemma tree-induction

∀[E:Type]. ∀[P:tree(E) ⟶ ℙ].
  ((∀value:E. P[tree_leaf(value)])
  ⇒ (∀left,right:tree(E).  (P[left] ⇒ P[right] ⇒ P[tree_node(left;right)]))
  ⇒ {∀v:tree(E). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}[P:tree(E)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}value:E.  P[tree\_leaf(value)])
    {}\mRightarrow{}  (\mforall{}left,right:tree(E).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[tree\_node(left;right)]))
    {}\mRightarrow{}  \{\mforall{}v:tree(E).  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index