An exact proof term for the current goal is omega_TransSet.

Let n be given.

Assume Hn: n ∈ ω.

We will prove TransSet n.

Apply ordinal_TransSet to the current goal.

We will prove ordinal n.

Apply nat_p_ordinal to the current goal.

We will prove nat_p n.

An exact proof term for the current goal is (omega_nat_p n Hn).