Function assumptions are only considered at the outermost level

[melvic-ybanez]

Prove the following proposition:

(A => (B => C)) => (A & B) => C)

With the current algorithm, the outermost antecedent (A => B => C) is not considered as valid assumption from which to draw a proof of C because the C antecedent of this function is within the function's antecedent itself.

(A => B => C) should be isomorphic to A & B => C so the proposition above should work, considering we have a A & B to supply to the outer antecedent.