I am proving various statements relating to applicative functors, using the Coq proof assistant (I am considering only Coq terms, which always terminate so you don't have to worry about _|_). However, I'm not sure how to go about proving a certain conjecture, which, translated back into Haskell and made more specific to make it easier to think about, looks like this (assuming Control.Applicative and Control.Arrow are imported): "For all applicative functors: \f x -> fmap second f <*> fmap ((,) (0::Int)) x is equivalent to \f x -> fmap ((,) (0::Int)) (f <*> x)" McBride and Patterson give four laws for applicative functors in their paper "Functional Pearl: Applicative programming with effects". Can these laws be used to prove this conjecture for all applicative functors satisfying those laws? -- Robin P.S. I realise this might not look like a "commutative diagram conjecture", but as I said, I've made it more specific - my actual conjecture is more general, but hopefully if I can understand how to prove the specific one, I'll be able to prove my real one in short order.