proposition: Lemma choose_spec1: forall s x, choose s = Some x -> In x s.
proof: Proof. induction s as [| l IHl o r IHr]; simpl. - intros. discriminate. - destruct o. + intros x H. injection H; intros; subst. reflexivity. + revert IHl. case choose. * intros p Hp x [= <-]. apply Hp. reflexivity. * intros _ x. revert IHr. case choose. -- intros p Hp [= <-]. apply Hp. reflexivity. -- intros. discriminate. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface