Let X and Y be given.

Assume Heq: equip X Y.

Assume Hfin: finite Y.

We will prove finite X.

We will prove ∃n ∈ ω, equip X n.

Apply Hfin to the current goal.

Let n be given.

Assume Hpair: n ∈ ω ∧ equip Y n.

We prove the intermediate claim Hn: n ∈ ω.

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

We prove the intermediate claim HeqYn: equip Y n.

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

We prove the intermediate claim HeqXn: equip X n.

An exact proof term for the current goal is (equip_tra X Y n Heq HeqYn).

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is HeqXn.

∎