proposition: Lemma choose_spec3 : choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y.
proof: Proof. exact (@M.choose_spec3 _ _ _ _ _ _). Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts