An exact proof term for the current goal is (λX y H ⇒ ReplE X Inj1 y H).