proposition: Corollary fmap_comp_x `{FunctorLaws F} : forall (a b c : Type) (f : b -> c) (g : a -> b) x, fmap f (fmap g x) = fmap (fun y => f (g y)) x.
proof: Proof. intros. replace (fun y : a => f (g y)) with (f \o g). rewrite <- fmap_comp. reflexivity. reflexivity. Qed.
imports: Hask.Ltac FunctionalExtensionality Coq.Classes.Morphisms Coq.Setoids.Setoid