I wonder whether the following holds in intuitionistic logic: $((P \to U \lor V) \to Z) \leftrightarrow ((P \to U) \to Z) \land ((P \to V) \to Z)$
For disjunction I assume the following two rules: $\begin{array}{lcl} \begin{array}{l} G\vdash U\\ \hline G\vdash U\lor V \end{array} &\quad& \text{(Rv1)}\\ &\\ \begin{array}{l} G\vdash V\\ \hline G\vdash U\lor V \end{array} &\quad& \text{(Rv2)}\\ &\\ \begin{array}{l} G,\ U\vdash A\\ G,\ V\vdash A\\ \hline G,\ U\lor V \vdash A \end{array} &\quad& \text{(Lv)}\end{array}$
I can easily proof the following direction: $((P \to U \lor V) \to Z) \to ((P \to U) \to Z) \land ((P \to V) \to Z)$
Namly we have: $\begin{array}{ll} U\vdash U\lor V\\ \hline P\to U\vdash P\to U\lor V\\ \hline (P\to U\lor V) \to Z\vdash (P\to U)\to Z \end{array}$
But I am not sure whether I can establish the other direction.
Bye
P.S.: I didn't try Kripke models or Weak conterexamples. I only tried proof theoretically to derive it, by the rules that I have given in my Question.
P.S.S.: It would give an alternative method to the Rip (Resolution for Intuitionistic Logic) found in Basic Proof Theory, Second Edition, Troelstra & Schwichtenberg, 2000, p.253.