proposition: Lemma eq_option_alt (o o':option elt) : o=o' <-> (forall e, o=Some e <-> o'=Some e).
proof: Proof. split; intros. - now subst. - destruct o, o'; rewrite ?H; auto. symmetry; now apply H. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)