Let n be given.
Assume HnO: n ∈ ω.
We will prove Romega_tilde n ≠ Empty.
Assume HEmpty: Romega_tilde n = Empty.
We will prove False.
We prove the intermediate claim H0in: Romega_zero ∈ Romega_tilde n.
An exact proof term for the current goal is (Romega_zero_in_Romega_tilde n HnO).
We prove the intermediate claim H0E: Romega_zero ∈ Empty.
rewrite the current goal using HEmpty (from right to left).
An exact proof term for the current goal is H0in.
An exact proof term for the current goal is (EmptyE Romega_zero H0E).
∎