---

Step * of Lemma aa_data_wrapper_ind_wf

[X:{j}]. [T:Type]. [x:aa_data_wrapper(T)]. [node:nd:aa_data_wrapper(T)  rec1:X  X]. [leaf:val:T  X].
  (aa_data_wrapper_ind(x;nd,rec1.node[nd;rec1];val.leaf[val])  X)
BY
{ DatatypeIndWf 1 `aa_data_wrapper` `aa_data_wrapper_ind`  }


\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[T:Type].  \mforall{}[x:aa\_data\_wrapper(T)].  \mforall{}[node:nd:aa\_data\_wrapper(T)  {}\mrightarrow{}  rec1:X  {}\mrightarrow{}  X].
\mforall{}[leaf:val:T  {}\mrightarrow{}  X].
    (aa\_data\_wrapper\_ind(x;nd,rec1.node[nd;rec1];val.leaf[val])  \mmember{}  X)


By

DatatypeIndWf  1  `aa\_data\_wrapper`  `aa\_data\_wrapper\_ind` 



Home Index