An exact proof term for the current goal is (λx : set ⇒ binunionI2 x {x} x (SingI x)).