Let A, F and x be given.

Assume H1.

Apply ReplEq A F (F x) to the current goal.

Assume _ H2.

Apply H2 to the current goal.

We will prove ∃x' ∈ A, F x = F x'.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is (λq H ⇒ H).

∎