proposition: Lemma fmap_endo_nothing {c} (f : c → c) (m : Maybe c) : f <$> m = Nothing <-> m = Nothing.
proof: Proof. induction m; simpl; intuition auto; discriminate. Qed.
imports: Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.Applicative.Proofs Category.Theory.Coq.Monad.Proofs Category.Theory.Coq.Maybe