Step
*
of Lemma
binary_map_size_wf
∀[T,Key:Type]. ∀[p:binary_map(T;Key)]. (binary_map_size(p) ∈ ℕ)
BY
{ ProveCoSizeWf2 `binary_mapco_size` }
Latex:
\mforall{}[T,Key:Type]. \mforall{}[p:binary\_map(T;Key)]. (binary\_map\_size(p) \mmember{} \mBbbN{})
By
ProveCoSizeWf2 `binary\_mapco\_size`
Home
Index