proposition: Corollary fmap_pure_x `{ApplicativeLaws m} : forall (a b : Type) (f : a -> b) x, fmap[m] f (pure x) = pure (f x).
proof: Proof. intros. replace (pure[m] (f x)) with ((pure[m] \o f) x). rewrite <- fmap_pure. reflexivity. reflexivity. Qed.
imports: Hask.Ltac Hask.Data.Functor Hask.Data.Functor.Const FunctionalExtensionality