Let F be given.
Assume HFfin: finite F.
Assume Hall: ∀A : set, A ∈ F → finite A.
Set p to be the term λF0 : set ⇒ (∀A : set, A ∈ F0 → finite A) → finite (⋃ F0).
We prove the intermediate claim HpEmpty: p Empty.
Assume Hall0: ∀A : set, A ∈ Empty → finite A.
rewrite the current goal using Union_Empty_eq (from left to right).
An exact proof term for the current goal is finite_Empty.
We prove the intermediate claim HpStep: ∀F0 y : set, finite F0 → y ∉ F0 → p F0 → p (F0 ∪ {y}).
Let F0 and y be given.
Assume HF0fin: finite F0.
Assume HyNot: y ∉ F0.
Assume IH: p F0.
Assume HallU: ∀A : set, A ∈ (F0 ∪ {y}) → finite A.
We prove the intermediate claim HallF0: ∀A : set, A ∈ F0 → finite A.
Let A be given.
Assume HA: A ∈ F0.
An exact proof term for the current goal is (HallU A (binunionI1 F0 {y} A HA)).
We prove the intermediate claim HFinUF0: finite (⋃ F0).
An exact proof term for the current goal is (IH HallF0).
We prove the intermediate claim HFinY: finite y.
An exact proof term for the current goal is (HallU y (binunionI2 F0 {y} y (SingI y))).
rewrite the current goal using (Union_binunion_singleton_eq F0 y) (from left to right).
An exact proof term for the current goal is (binunion_finite (⋃ F0) HFinUF0 y HFinY).
We prove the intermediate claim HpF: p F.
An exact proof term for the current goal is (finite_ind p HpEmpty HpStep F HFfin).
An exact proof term for the current goal is (HpF Hall).
∎