Apply finite_ind to the current goal.
Let Y be given.
Assume H1: Y ⊆ 0.
We will prove finite Y.
rewrite the current goal using Empty_Subq_eq Y H1 (from left to right).
An exact proof term for the current goal is finite_Empty.
Let X and z be given.
Assume HX: finite X.
Assume Hz: z ∉ X.
Assume IH: ∀Y, Y ⊆ X → finite Y.
Let Y be given.
Assume H1: Y ⊆ X ∪ {z}.
We will prove finite Y.
Apply xm (z ∈ Y) to the current goal.
Assume H2: z ∈ Y.
We prove the intermediate claim L1: Y = (Y ∖ {z}) ∪ {z}.
Apply set_ext to the current goal.
Let w be given.
Assume Hw: w ∈ Y.
Apply xm (w ∈ {z}) to the current goal.
Assume H3: w ∈ {z}.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is H3.
Assume H3: w ∉ {z}.
Apply binunionI1 to the current goal.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw: w ∈ (Y ∖ {z}) ∪ {z}.
Apply binunionE (Y ∖ {z}) {z} w Hw to the current goal.
Assume H3: w ∈ Y ∖ {z}.
An exact proof term for the current goal is setminusE1 Y {z} w H3.
Assume H3: w ∈ {z}.
We will prove w ∈ Y.
rewrite the current goal using SingE z w H3 (from left to right).
An exact proof term for the current goal is H2.
rewrite the current goal using L1 (from left to right).
Apply adjoin_finite to the current goal.
We will prove finite (Y ∖ {z}).
Apply IH to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∖ {z}.
Apply setminusE Y {z} y Hy to the current goal.
Assume Hy1: y ∈ Y.
Assume Hy2: y ∉ {z}.
We will prove y ∈ X.
Apply binunionE X {z} y (H1 y Hy1) to the current goal.
Assume H3: y ∈ X.
An exact proof term for the current goal is H3.
Assume H3: y ∈ {z}.
We will prove False.
Apply Hy2 to the current goal.
An exact proof term for the current goal is H3.
Assume H2: z ∉ Y.
Apply IH to the current goal.
Let y be given.
Assume Hy: y ∈ Y.
We will prove y ∈ X.
Apply binunionE X {z} y (H1 y Hy) to the current goal.
Assume H3: y ∈ X.
An exact proof term for the current goal is H3.
Assume H3: y ∈ {z}.
We will prove False.
Apply H2 to the current goal.
We will prove z ∈ Y.
rewrite the current goal using SingE z y H3 (from right to left).
An exact proof term for the current goal is Hy.
∎