We will prove finite (X ∪ 0).

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

An exact proof term for the current goal is HX.

Let Y and z be given.

Assume HY: finite Y.

Assume Hz: z ∉ Y.

Assume IH: finite (X ∪ Y).

We will prove finite (X ∪ (Y ∪ {z})).

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

We will prove finite ((X ∪ Y) ∪ {z}).

Apply adjoin_finite to the current goal.

An exact proof term for the current goal is IH.