Let A, F and y be given.

Apply ReplEq A F y to the current goal.

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

∎