proposition: Corollary fmap_pure `{ApplicativeLaws m} : forall (a b : Type) (f : a -> b), fmap[m] f \o pure = pure \o f.
proof: Proof. intros a b f. extensionality x. unfold Basics.compose. rewrite <- ap_fmap. apply ap_homo. Qed.
imports: Hask.Ltac Hask.Data.Functor Hask.Data.Functor.Const FunctionalExtensionality