proposition: Lemma eq_option_alt {A}(o o':option A) : o=o' <-> (forall x, o=Some x <-> o'=Some x).
proof: Proof. split; intros. - now subst. - destruct o, o'; rewrite ?H; auto. symmetry; now apply H. Qed.
imports: Coq(List SetoidList)