Let Y and y be given.

Assume HYfin: finite Y.

Assume HyNot: y ∉ Y.

Assume HImgFin: finite {F x|x ∈ Y}.

Set ImgY to be the term {F x|x ∈ Y}.

We prove the intermediate claim HImgYyFin: finite (ImgY ∪ {F y}).

An exact proof term for the current goal is (adjoin_finite ImgY (F y) HImgFin).

We prove the intermediate claim Hsub: {F x|x ∈ (Y ∪ {y})} ⊆ (ImgY ∪ {F y}).

Let z be given.

Assume Hz: z ∈ {F x|x ∈ (Y ∪ {y})}.

We will prove z ∈ (ImgY ∪ {F y}).

Apply (ReplE_impred (Y ∪ {y}) F z Hz) to the current goal.

Let x be given.

Assume HxYy: x ∈ (Y ∪ {y}).

Assume HzEq: z = F x.

Apply (binunionE Y {y} x HxYy) to the current goal.

Assume HxY: x ∈ Y.

We prove the intermediate claim HzImg: z ∈ ImgY.

rewrite the current goal using HzEq (from left to right).

An exact proof term for the current goal is (ReplI Y F x HxY).

An exact proof term for the current goal is (binunionI1 ImgY {F y} z HzImg).

Assume Hxy: x ∈ {y}.

We prove the intermediate claim HxEq: x = y.

An exact proof term for the current goal is (SingE y x Hxy).

We prove the intermediate claim HzFy: z = F y.

rewrite the current goal using HxEq (from right to left).

An exact proof term for the current goal is HzEq.

rewrite the current goal using HzFy (from left to right).

An exact proof term for the current goal is (binunionI2 ImgY {F y} (F y) (SingI (F y))).

An exact proof term for the current goal is (Subq_finite (ImgY ∪ {F y}) HImgYyFin {F x|x ∈ (Y ∪ {y})} Hsub).