A tactic for cleaning hypothesis after use of functional induction.
Encapsulation
We can implement
S with balanced binary search trees.
When compared to
FSetAVL, we maintain here two invariants
(bst and avl) instead of only bst, which is enough for fulfilling
the FSet interface.
This encapsulation propose the non-structural variants
ocaml_union,
ocaml_subset,
ocaml_compare,
ocaml_equal.