---

Step * of Lemma MMTree-induction

∀[T:Type]. ∀[P:MMTree(T) ⟶ ℙ].
  ((∀val:T. P[MMTree_Leaf(val)])
  ⇒ (∀forest:MMTree(T) List List. ((∀u∈forest.(∀u1∈u.P[u1])) ⇒ P[MMTree_Node(forest)]))
  ⇒ {∀v:MMTree(T). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:MMTree(T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}val:T.  P[MMTree\_Leaf(val)])
    {}\mRightarrow{}  (\mforall{}forest:MMTree(T)  List  List.  ((\mforall{}u\mmember{}forest.(\mforall{}u1\mmember{}u.P[u1]))  {}\mRightarrow{}  P[MMTree\_Node(forest)]))
    {}\mRightarrow{}  \{\mforall{}v:MMTree(T).  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index