Let alpha, x and y be given.
Assume Hxy.
An exact proof term for the current goal is Hxy.
∎