proposition: Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' -> (equal cmp s s' = true <-> Equivb s s').
proof: Proof. intros s s' B B'. rewrite Equivb_elements, <- equal_IfEq. split; [apply L.equal_2|apply L.equal_1]; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int