proposition: Lemma choose_3 : forall s s' x x', choose s = Some x -> choose s' = Some x' -> Equal s s' -> E.eq x x'.
proof: Proof. unfold choose; intros. generalize (M.choose_equal H1); clear H1. destruct (M.choose s) as [(?,?)|?]; destruct (M.choose s') as [(?,?)|?]; simpl; auto; congruence. Qed.
imports: FSetInterface