An exact proof term for the current goal is (λ(y : set)(H1 : y ∈ x) ⇒ binunionI1 x {x} y H1).