Let n be given.

Assume Hn: n ∈ ω.

Let m be given.

Assume Hm: m ∈ n.

We will prove m ∈ ω.

Apply nat_p_omega to the current goal.

We will prove nat_p m.

Apply (nat_p_trans n) to the current goal.

We will prove nat_p n.

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

We will prove m ∈ n.

An exact proof term for the current goal is Hm.

∎