Let F and y be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ (F ∪ {y}).
We will prove x ∈ (⋃ F) ∪ y.
Apply (UnionE_impred (F ∪ {y}) x Hx (x ∈ (⋃ F) ∪ y)) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HU: U ∈ (F ∪ {y}).
Apply (binunionE F {y} U HU (x ∈ (⋃ F) ∪ y)) to the current goal.
Assume HU_F: U ∈ F.
An exact proof term for the current goal is (binunionI1 (⋃ F) y x (UnionI F x U HxU HU_F)).
Assume HU_sing: U ∈ {y}.
We prove the intermediate claim HUeq: U = y.
An exact proof term for the current goal is (SingE y U HU_sing).
We prove the intermediate claim Hxy: x ∈ y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (binunionI2 (⋃ F) y x Hxy).
Let x be given.
Assume Hx: x ∈ (⋃ F) ∪ y.
We will prove x ∈ ⋃ (F ∪ {y}).
Apply (binunionE (⋃ F) y x Hx (x ∈ ⋃ (F ∪ {y}))) to the current goal.
Assume HxUF: x ∈ ⋃ F.
Apply (UnionE_impred F x HxUF (x ∈ ⋃ (F ∪ {y}))) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HU_F: U ∈ F.
An exact proof term for the current goal is (UnionI (F ∪ {y}) x U HxU (binunionI1 F {y} U HU_F)).
Assume Hxy: x ∈ y.
An exact proof term for the current goal is (UnionI (F ∪ {y}) x y Hxy (binunionI2 F {y} y (SingI y))).
∎