proposition: Lemma choose_ok1 : forall s x, M.choose s = Some x <-> exists H:In x s, choose s = inleft _ (exist (fun x => In x s) x H).
proof: Proof. intros s x. unfold choose; split; intros. - destruct (choose_aux s) as [(y,Hy)|H']; try congruence. replace x with y in * by congruence. exists (choose_1 Hy); auto. - destruct H. destruct (choose_aux s) as [(y,Hy)|H']; congruence. Qed.
imports: FSetInterface