---

Step * of Lemma aa_data_wrapper-induction

[T:Type]. [P:aa_data_wrapper(T)  ].
  ((nd:aa_data_wrapper(T). (P[nd]  P[aa_data_wrapnode(nd)]))
   (val:T. P[aa_data_wrapleaf(val)])
   {x:aa_data_wrapper(T). P[x]})
BY
{ DatatypeInductionAux ``aa_data_wrapper aa_data_wrapnode aa_data_wrapleaf`` }


\mforall{}[T:Type].  \mforall{}[P:aa\_data\_wrapper(T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}nd:aa\_data\_wrapper(T).  (P[nd]  {}\mRightarrow{}  P[aa\_data\_wrapnode(nd)]))
    {}\mRightarrow{}  (\mforall{}val:T.  P[aa\_data\_wrapleaf(val)])
    {}\mRightarrow{}  \{\mforall{}x:aa\_data\_wrapper(T).  P[x]\})


By

DatatypeInductionAux  ``aa\_data\_wrapper  aa\_data\_wrapnode  aa\_data\_wrapleaf``



Home Index