Assume H2: y ∈ X.

We prove the intermediate claim L1: X = (X ∖ {y}) ∪ {y}.

An exact proof term for the current goal is binunion_remove1_eq X y H2.

Apply HX to the current goal.

We will prove finite X.

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

Apply binunion_finite to the current goal.

An exact proof term for the current goal is H1.

Apply Sing_finite to the current goal.

Assume H2: y ∉ X.

We prove the intermediate claim L2: X = X ∖ {y}.

Apply set_ext to the current goal.

We will prove X ⊆ X ∖ {y}.

Let x be given.

Assume Hx: x ∈ X.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hx.

Assume H3: x ∈ {y}.

Apply H2 to the current goal.

We will prove y ∈ X.

rewrite the current goal using SingE y x H3 (from right to left).

An exact proof term for the current goal is Hx.

Apply setminus_Subq to the current goal.

Apply HX to the current goal.

We will prove finite X.

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

An exact proof term for the current goal is H1.