[Haskell-cafe] A "commutative diagram" conjecture about applicative functors

[Robin Green]

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.