Step
*
of Lemma
aa_bst_member_wf
[t:aa_ltree(
)].
[i:
].
(aa_bst_member(i;t)
)
BY
{
ProveWfLemma
}
\mforall{}[t:aa\_ltree(\mBbbZ{})]. \mforall{}[i:\mBbbZ{}]. (aa\_bst\_member(i;t) \mmember{} \mBbbB{})
By
ProveWfLemma
Home
Index
[t:aa_ltree(
)]. [i:]. (aa_bst_member(i;t) 
)