Let X be given.
Apply nat_ind to the current goal.
Assume _.
We will prove finite (⋃i ∈ 0X i).
rewrite the current goal using famunion_Empty (from left to right).
An exact proof term for the current goal is finite_Empty.
Let n be given.
Assume Hn.
Assume IHn: (∀i ∈ n, finite (X i)) → finite (⋃i ∈ nX i).
Assume H1: ∀i ∈ ordsucc n, finite (X i).
We will prove finite (⋃i ∈ ordsucc nX i).
We prove the intermediate claim L1: (⋃i ∈ ordsucc nX i) = (⋃i ∈ nX i) ∪ X n.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ ⋃i ∈ ordsucc nX i.
Apply famunionE_impred (ordsucc n) X z Hz to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume H2: z ∈ X i.
Apply ordsuccE n i Hi to the current goal.
Assume H3: i ∈ n.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is famunionI n X i z H3 H2.
Assume H3: i = n.
Apply binunionI2 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H2.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz.
Apply famunionE_impred n X z Hz to the current goal.
Let i be given.
Assume Hi: i ∈ n.
Assume H2: z ∈ X i.
Apply famunionI (ordsucc n) X i z to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is H2.
Assume Hz.
Apply famunionI (ordsucc n) X n z to the current goal.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is Hz.
rewrite the current goal using L1 (from left to right).
We will prove finite ((⋃i ∈ nX i) ∪ X n).
Apply binunion_finite to the current goal.
Apply IHn to the current goal.
Let i be given.
Assume Hi: i ∈ n.
Apply H1 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
Apply H1 n to the current goal.
Apply ordsuccI2 to the current goal.
∎