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