We will prove 2 ∈ ω ∖ {0}.
We prove the intermediate claim H2omega: 2 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 2 nat_2).
We prove the intermediate claim H2not0: 2 ∉ {0}.
Assume H2: 2 ∈ {0}.
We will prove False.
We prove the intermediate claim Heq: 2 = 0.
An exact proof term for the current goal is (SingE 0 2 H2).
An exact proof term for the current goal is (neq_2_0 Heq).
An exact proof term for the current goal is (setminusI ω {0} 2 H2omega H2not0).
∎