An exact proof term for the current goal is (λu p H1 H2 H3 ⇒ u p (λu ⇒ u p H1 H2) H3).