---

Step * of Lemma tree-definition

∀[E,A:Type]. ∀[R:A ⟶ tree(E) ⟶ ℙ].
  ((∀value:E. {x:A| R[x;tree_leaf(value)]} )
  ⇒ (∀left,right:tree(E).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;tree_node(left;right)]} ))
  ⇒ {∀v:tree(E). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `tree-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `tree-induction`

---

Home Index