Let P and f be given.
Assume H1.
An exact proof term for the current goal is Repl_inv_eq P f f H1.
∎