---

Step * of Lemma aa_ltree_wf

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


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


By

Unfold  `aa\_ltree`  0  THEN  Auto



Home Index