---

Step * of Lemma aa_lt_node?_wf

[T:Type]. [x:aa_ltree(T)].  (aa_lt_node?(x)  )
BY
{ Auto THEN RW (AddrC [2] (UnfoldTopAbC)) 0 THEN Auto }


\mforall{}[T:Type].  \mforall{}[x:aa\_ltree(T)].    (aa\_lt\_node?(x)  \mmember{}  \mBbbB{})


By

Auto  THEN  RW  (AddrC  [2]  (UnfoldTopAbC))  0  THEN  Auto



Home Index