Let X, g and h be given.
Assume H1: ∀x ∈ X, g x = h x.
We will prove F X g = F X h.
Apply xm (⋃ X ∈ X) to the current goal.
Assume H2: (⋃ X ∈ X).
We will prove (if ⋃ X ∈ X then f (⋃ X) (g (⋃ X)) else z) = (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z).
rewrite the current goal using (H1 (⋃ X) H2) (from left to right).
We will prove (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z) = (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z).
An exact proof term for the current goal is (λq H ⇒ H).
Assume H2: ¬ (⋃ X ∈ X).
We will prove (if ⋃ X ∈ X then f (⋃ X) (g (⋃ X)) else z) = (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z).
We prove the intermediate claim L1: (if ⋃ X ∈ X then f (⋃ X) (g (⋃ X)) else z) = z.
An exact proof term for the current goal is (If_i_0 (⋃ X ∈ X) (f (⋃ X) (g (⋃ X))) z H2).
We prove the intermediate claim L2: (if ⋃ X ∈ X then f (⋃ X) (h (⋃ X)) else z) = z.
An exact proof term for the current goal is (If_i_0 (⋃ X ∈ X) (f (⋃ X) (h (⋃ X))) z H2).
rewrite the current goal using L2 (from left to right).
An exact proof term for the current goal is L1.
∎