Let A, B and x be given.

Assume HAB Hx.

An exact proof term for the current goal is (HAB x Hx).

∎