proposition: Lemma choose_equal : forall s s', Equal s s' -> match choose s, choose s' with | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x' | inright _, inright _ => True | _, _ => False end.
proof: Proof. intros. generalize (@M.choose_1 s)(@M.choose_2 s) (@M.choose_1 s')(@M.choose_2 s')(@M.choose_3 s s') (choose_ok1 s)(choose_ok2 s)(choose_ok1 s')(choose_ok2 s'). destruct (choose s) as [(x,Hx)|Hx]; destruct (choose s') as [(x',Hx')|Hx']; auto; intros. - apply H4; auto. + rewrite H5; exists Hx; auto. + rewrite H7; exists Hx'; auto. - apply Hx' with x; unfold Equal in H; rewrite <-H; auto. - apply Hx with x'; unfold Equal in H; rewrite H; auto. Qed.
imports: FSetInterface