can λ-prolog do it? (Was: How to prove this theorem with intuitionistic natural deduction?)

Hi,
Can λ-prolog do it? The proof is a little bit
tricky, since line 1 is used twice in
line 2 and in line 4. So its not a proof
tree, rather a proof mesh (*). What would λ-prolog
give via curry howard? If we would use something
along these lines:
https://en.wikipedia.org/wiki/%CE%9BProlog#Programming_in_%CE%BBProlog
The proof search is loosely from the book
figure 9.6 Programming in Higher-Order Logic
from Miler and Nadathur.
Bye
(*) Displayed in Fitch Style.
Julio Di Egidio schrieb:

On 18/11/2024 23:22, Mild Shock wrote:

Julio Di Egidio schrieb:

`(P -> Q -> R) |- (P /\ Q -> R)`

0: P -> (Q -> R) (Premisse)
1: P /\ Q        (Assumption)
2: P             (/\E,1)
3: Q -> R        (->E,0,2)
4: Q             (/\E,1)
5: R             (->E,3,4)
6: P /\ Q -> R   (Discharge,1)

 Wonderful, thank you.
 -Julio