Program equivalence:
p in (A => B) is equivalent to q in (A => B) exactly when p(x) = q(x) for all x in A.

Definition of =, if you need that:
forAll a. a = a.
(a = b) => (b = a)
(a = c) => (c = b) => (a = b).

If there's anything else I can help you with, just holler.

On documentation: if you're implementing (A => B) => (C => A) => C => B for all A B C,
and your program does anything other than compose two functions, then you either document that or you lie.
If it is mere composition, then the type is a complete and unambiguous specification of the function.