An exact proof term for the current goal is (λx y H ⇒ UPairE y x x H (y = x) (λH ⇒ H) (λH ⇒ H)).