Let X, f and p be given.

Assume H1.

Let y be given.

Assume Hy.

Apply ReplE_impred X f y Hy to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hx2: y = f x.

We will prove p y.

rewrite the current goal using Hx2 (from left to right).

An exact proof term for the current goal is H1 x Hx.

∎