---

Step * of Lemma aa_lt_node_wf

[T:Type]. [val:T]. [left_subtree,right_subtree:aa_ltree(T)].
  (aa_lt_node(val;left_subtree;right_subtree)  aa_ltree(T))
BY
{ Unfolds ``aa_ltree aa_lt_node`` 0 THEN Auto THEN MemTypeCD THEN Auto }


\mforall{}[T:Type].  \mforall{}[val:T].  \mforall{}[left$_{subtree}$,right$_{subtree}$:aa\000C\_ltree(T)].
    (aa\_lt\_node(val;left$_{subtree}$;right$_{subtree}$)  \mmember{}  aa\_l\000Ctree(T))


By

Unfolds  ``aa\_ltree  aa\_lt\_node``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto



Home Index