proposition: Theorem foldr_fmap_fusion `{Foldable t} `{FunctorLaws t} : forall A B (f : A -> B -> B) C (g : C -> A) (z : B) (xs : t C), foldr f z (fmap g xs) = foldr (f \o g) z xs.
proof: Proof. intros. pose proof (foldr_parametricity C B (f \o g) z A B f z g id eq_refl (fun _ _ => eq_refl)). replace (foldr f z (fmap[ t] g xs)) with ((foldr f z \o fmap[ t] g) xs) by trivial. rewrite <- H2. reflexivity. Qed.
imports: Hask.Ltac Hask.Data.Functor