Let X, n and f be given.
Assume Hnat: nat_p n.
Assume Hinj: inj X n f.
We will prove finite X.
Set Img to be the term {f x|x ∈ X}.
We prove the intermediate claim Heq: equip X Img.
An exact proof term for the current goal is (inj_equip_image X n f Hinj).
We prove the intermediate claim Hsub: Img ⊆ n.
Let y be given.
Assume Hy: y ∈ Img.
We will prove y ∈ n.
Apply (ReplE_impred X (λx0 : set ⇒ f x0) y Hy (y ∈ n)) to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hyx: y = f x.
We prove the intermediate claim Hcod: ∀u ∈ X, f u ∈ n.
An exact proof term for the current goal is (andEL (∀u ∈ X, f u ∈ n) (∀u v ∈ X, f u = f v → u = v) Hinj).
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is (Hcod x Hx).
We prove the intermediate claim Hfinn: finite n.
An exact proof term for the current goal is (nat_finite n Hnat).
We prove the intermediate claim HfinImg: finite Img.
An exact proof term for the current goal is (Subq_finite n Hfinn Img Hsub).
An exact proof term for the current goal is (equip_finite_transfer X Img Heq HfinImg).
∎