proposition: Lemma choose_ok2 : forall s, M.choose s = None <-> exists H:Empty s, choose s = inright _ H.
proof: Proof. intros s. unfold choose; split; intros. - destruct (choose_aux s) as [(y,Hy)|H']; try congruence. exists (choose_2 H'); auto. - destruct H. destruct (choose_aux s) as [(y,Hy)|H']; congruence. Qed.
imports: FSetInterface