proposition: Lemma choose_equal : forall s s', Equal s s' -> match choose s, choose s' with | Some x, Some x' => E.eq x x' | None, None => True | _, _ => False end.
proof: Proof. intros s s' H; generalize (@choose_1 s)(@choose_2 s) (@choose_1 s')(@choose_2 s')(@choose_3 s s'); destruct (choose s); destruct (choose s'); simpl; intuition. - apply H5 with e; rewrite <-H; auto. - apply H5 with e; rewrite H; auto. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide