An exact proof term for the current goal is (λu p H ⇒ u p (λu u3 ⇒ u p (λu1 u2 ⇒ H u1 u2 u3))).