We will prove ¬ (0 ∈ Zplus).
Assume H0: 0 ∈ Zplus.
We will prove False.
We prove the intermediate claim H0m: 0 ∈ ω ∖ {0}.
An exact proof term for the current goal is H0.
We prove the intermediate claim Hcore: 0 ∈ ω ∧ 0 ∉ {0}.
An exact proof term for the current goal is (setminusE ω {0} 0 H0m).
We prove the intermediate claim H0not: 0 ∉ {0}.
An exact proof term for the current goal is (andER (0 ∈ ω) (0 ∉ {0}) Hcore).
An exact proof term for the current goal is (H0not (SingI 0)).
∎