Let α, x and y be given.

Assume Hxy.

An exact proof term for the current goal is Hxy.

∎