Gödel showed that proofs are strategies in a game.

 We write $A_D( x; y)$ with $x,y$ lists of typed variables interpreted as follows. The variables in $y$ represent the type of a challenge to formula $A$ and those in $x$ represent the type of a defense of $A$. A proof of $A$ amounts to a term $t(y)$(functional) which expresses that every challenge can be answered.

Now suppose we have $A_D(x;y)$ and $B_D(v;w)$ and we consider $A \rightarrow B$. Then a challenge to the implication must consist in defending $A$ and at the same time challenging $B$. Thus it has template the list $x,w$. The defense, given such a $x;w$ must consist in a defense of $B$ given the defense $x$ of $A$ (a functional $g(x)$) and in a challenge to $A$ given its defense $x$ and the challenge $w$ to $B$ (a functional $f(x,w)$). Thus $(A\rightarrow B)_D(f,g; x,w) \equiv A_D(x; fxw) \rightarrow B_D(gx, w)$.  Note that $f$ depends on $x$ and $w$ because we are only interested in challenging $A$ if the opponent is at once defending $A$ through $x$ and challenging $B$ through $w$. On the other hand it is enough for the opponent to defend $A$ though $x$ for us to need to defend $B$.