Apply In_ind to the current goal.
Let X be given.
Let Y and Z be given.
We prove the intermediate
claim L1:
∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Y = F X f.
We prove the intermediate
claim L2:
∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Z = F X f.
Let g be given.
Let h be given.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using H6 (from left to right).
We will
prove F X g = F X h.
Apply Fr to the current goal.
We will
prove ∀x ∈ X, g x = h x.
Let x be given.
An exact proof term for the current goal is (IH x H7 (g x) (h x) (H3 x H7) (H5 x H7)).
∎