proposition: Lemma option_map_None A B (f : A -> B) x : option_map f x = None <-> x = None.
proof: Proof. destruct x; simpl; split; intros; trivial; congruence. Qed.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat