fact: Definition option_eq {A} eq (x y : option A) := match x with | None => y = None | Some ax => match y with | None => False | Some ay => eq ax ay end end.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat