Let J, f and g be given.
Assume HJne: J ≠ Empty.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
Apply (nonempty_has_element J HJne) to the current goal.
Let j0 be given.
Assume Hj0: j0 ∈ J.
Set a0 to be the term power_real_coord_clipped_diff f g j0.
We use a0 to witness the existential quantifier.
We will prove a0 ∈ power_real_clipped_diffs J f g.
We prove the intermediate claim Hdef: power_real_clipped_diffs J f g = Repl J (λj : set ⇒ power_real_coord_clipped_diff f g j).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (ReplI J (λj : set ⇒ power_real_coord_clipped_diff f g j) j0 Hj0).
∎