Step
*
of Lemma
bst_leaf?_wf
∀[E:Type]. ∀[v:bs_tree(E)]. (bst_leaf?(v) ∈ 𝔹)
BY
{ DepprodCoDatatypeRecognizerWf }
Latex:
Latex:
\mforall{}[E:Type]. \mforall{}[v:bs\_tree(E)]. (bst\_leaf?(v) \mmember{} \mBbbB{})
By
Latex:
DepprodCoDatatypeRecognizerWf
Home
Index