---

Step * of Lemma aa_lt_leaf_wf

[T:Type]. (aa_lt_leaf()  aa_ltree(T))
BY
{ Unfolds ``aa_ltree aa_lt_leaf`` 0 THEN Auto THEN MemTypeCD THEN Auto }


\mforall{}[T:Type].  (aa\_lt\_leaf()  \mmember{}  aa\_ltree(T))


By

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



Home Index