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