---

Step * of Lemma aa_ltree_ind_wf

[X:{j}]. [T:Type]. [x:aa_ltree(T)]. [leaf:X]. [node:val:T
                                                           left_subtree:aa_ltree(T)
                                                           right_subtree:aa_ltree(T)
                                                           rec1:X
                                                           rec2:X
                                                           X].
  (aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2])  X)
BY
{ DatatypeIndWf 1 `aa_ltree` `aa_ltree_ind`  }


\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[T:Type].  \mforall{}[x:aa\_ltree(T)].  \mforall{}[leaf:X].  \mforall{}[node:val:T
                                                                                                                    {}\mrightarrow{}  left$_{subtree}$:aa\000C\_ltree(T)
                                                                                                                    {}\mrightarrow{}  right$_{subtree}$:a\000Ca\_ltree(T)
                                                                                                                    {}\mrightarrow{}  rec1:X
                                                                                                                    {}\mrightarrow{}  rec2:X
                                                                                                                    {}\mrightarrow{}  X].
    (aa\_ltree\_ind(x;leaf;val,left$_{subtree}$,right$_{subtree}\mbackslash{}ff2\000C4,rec1,rec2.node[val;left$_{subtree}$;...;rec1;rec2])
      \mmember{}  X)


By

DatatypeIndWf  1  `aa\_ltree`  `aa\_ltree\_ind` 



Home Index