Let x be given.

Assume Hx.

Apply real_E x Hx to the current goal.

Assume _ _ _ _ _ Hx6 _.

An exact proof term for the current goal is Hx6.

∎