An exact proof term for the current goal is (λ(X x : set)(H : x ∈ Empty) ⇒ EmptyE x H (x ∈ X)).