An exact proof term for the current goal is (λX Y z H1 H2 H3 ⇒ H2 (H1 z H3)).