I am currently trying to wrap my head around intuitionistic logic and its interpretation using the curry-howard isomorphism and propositions as types.
I came about this explained relation between $\forall$ and $\rightarrow$:
A function type $s \rightarrow t$ is actually a function type $\forall x:s.t$ where the variable x does not occur in t. [..] Moreover, if we have a type $\forall x:s.t$ where x does not occur in t, we can omit x and just write $s\rightarrow t$ without losing information.
I do not get how this can work as I understand a $\rightarrow$ basically as "give me a proof of s and I give you a proof of t" - a mapping function. However, a function that maps needs a parameter, in this case the x which is a proof of s : $f(x):s\rightarrow t$. How can I still have a mapping if I am 'not allowed' to use x and thus any information contained in it anymore?
If I use an example: e.g. proof that every $\mathbb{N}$ is $\mathbb{R}$ I need to use the information contained in the proof that a given number is in $\mathbb{N}$ to show that $\mathbb{N}$ is more restrictive than $\mathbb{R}$ and thus any $\mathbb{N}$ has to be $\mathbb{R}$. However, I do not have 'access' to those information as x (the proof that the number is in $\mathbb{N}$) does not occur in my proof that the number is also $\mathbb{R}$.