proposition: Lemma eq_option_alt : forall (elt:Type)(o o':option elt), o=o' <-> (forall e, o=Some e <-> o'=Some e).
proof: Proof. split; intros. subst; split; auto. destruct o; destruct o'; try rewrite H; auto. symmetry; rewrite <- H; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses