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