---

Step * of Lemma tree_ind_wf_simple

No Annotations
∀[E,A:Type]. ∀[v:tree(E)]. ∀[leaf:value:E ⟶ A]. ∀[node:left:tree(E) ⟶ right:tree(E) ⟶ A ⟶ A ⟶ A].
  (tree_ind(v;
            tree_leaf(value)⇒ leaf[value];
            tree_node(left,right)⇒ rec1,rec2.node[left;right;rec1;rec2])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 1 `tree_ind_wf` }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[E,A:Type].  \mforall{}[v:tree(E)].  \mforall{}[leaf:value:E  {}\mrightarrow{}  A].
\mforall{}[node:left:tree(E)  {}\mrightarrow{}  right:tree(E)  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (tree\_ind(v;
                        tree\_leaf(value){}\mRightarrow{}  leaf[value];
                        tree\_node(left,right){}\mRightarrow{}  rec1,rec2.node[left;right;rec1;rec2])    \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  1  `tree\_ind\_wf`

---

Home Index