We prove the intermediate claim L1: ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → {0} ∪ {g x|x ∈ X} = {0} ∪ {h x|x ∈ X}.

Let X, g and h be given.

Assume H: ∀x ∈ X, g x = h x.

We prove the intermediate claim L1a: {g x|x ∈ X} = {h x|x ∈ X}.

An exact proof term for the current goal is (ReplEq_ext X g h H).

We will prove {0} ∪ {g x|x ∈ X} = {0} ∪ {h x|x ∈ X}.

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

Use reflexivity.

An exact proof term for the current goal is (In_rec_i_eq (λX f ⇒ {0} ∪ {f x|x ∈ X}) L1).