Assume H: {1} ∈ ω.
We will prove False.
We prove the intermediate claim Hnat: nat_p {1}.
An exact proof term for the current goal is (omega_nat_p {1} H).
We prove the intermediate claim Hord: ordinal {1}.
An exact proof term for the current goal is (nat_p_ordinal {1} Hnat).
We prove the intermediate claim Htr: TransSet {1}.
An exact proof term for the current goal is (ordinal_TransSet {1} Hord).
An exact proof term for the current goal is (not_TransSet_singleton_1 Htr).
∎