---

Step * of Lemma MMTree-definition

∀[T,A:Type]. ∀[R:A ─→ MMTree(T) ─→ ℙ].
  ((∀val:T. {x:A| R[x;MMTree_Leaf(val)]} )
  ⇒ (∀forest:MMTree(T) List List. ((∀u∈forest.(∀u1∈u.{x:A| R[x;u1]} )) ⇒ {x:A| R[x;MMTree_Node(forest)]} ))
  ⇒ {∀v:MMTree(T). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `MMTree-induction` }

---

Latex:


\mforall{}[T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  MMTree(T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}val:T.  \{x:A|  R[x;MMTree\_Leaf(val)]\}  )
    {}\mRightarrow{}  (\mforall{}forest:MMTree(T)  List  List
                ((\mforall{}u\mmember{}forest.(\mforall{}u1\mmember{}u.\{x:A|  R[x;u1]\}  ))  {}\mRightarrow{}  \{x:A|  R[x;MMTree\_Node(forest)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:MMTree(T).  \{x:A|  R[x;v]\}  \})


By

ProveDatatypeDefinition  `MMTree-induction`

---

Home Index