Let n be given.
We prove the intermediate
claim Hcore:
n ∈ ω ∧ n ∉ {0}.
An
exact proof term for the current goal is
(setminusE ω {0} n Hn).
We prove the intermediate
claim Hnnot0:
n ∉ {0}.
An
exact proof term for the current goal is
(andER (n ∈ ω) (n ∉ {0}) Hcore).
We prove the intermediate
claim HnIn:
n ∈ {0}.
rewrite the current goal using Heq (from left to right).
An
exact proof term for the current goal is
(SingI 0).
An exact proof term for the current goal is (Hnnot0 HnIn).
∎