Oftentimes in math we see statements of the form $P \to (Q \vee R)$. To prove them we can assume $P$ is true and $R$ is false, and then demonstrate that $Q$ is true. This method of proof has the form: $$ [ (P \wedge \neg R) \to Q ] \to [ P \to ( Q \vee R ) ]. $$ It seems to me this would be valid in a constructive type theory. I would have a function type, $H$, that takes $(p,f):P \wedge \neg R$ and gives $H(p,f):Q$. To prove the above proof method, I would have to obtain from such a function another function, $g$, such that $g(p):Q \vee R$ when $p:P$. This seems impossible, since the data that $H$ requires is both $p:P$ and $f:\neg R$.
Is this form of argument not valid in constructive type theory?