Let X be given.

Assume Hfin.

Apply Hfin to the current goal.

Let n be given.

Assume Hpair: n ∈ ω ∧ equip X n.

We prove the intermediate claim Hn: n ∈ ω.

An exact proof term for the current goal is (andEL (n ∈ ω) (equip X n) Hpair).

We prove the intermediate claim Heq: equip X n.

An exact proof term for the current goal is (andER (n ∈ ω) (equip X n) Hpair).

We prove the intermediate claim Hn_sub: n ⊆ ω.

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

We prove the intermediate claim Hcount_n: atleastp n ω.

An exact proof term for the current goal is (Subq_atleastp n ω Hn_sub).

We prove the intermediate claim Hcount_X: atleastp X n.

An exact proof term for the current goal is (equip_atleastp X n Heq).

An exact proof term for the current goal is (atleastp_tra X n ω Hcount_X Hcount_n).

∎