An exact proof term for the current goal is (Repl_Empty Inj1).