Let x and y be given.

Assume H.

An exact proof term for the current goal is (SingE y x H).

∎