Let x be given.

Assume Hx.

Apply real_E x Hx to the current goal.

Assume Hx1 _ _ _ _ _ _.

An exact proof term for the current goal is Hx1.

∎