Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, ∀y z : set, In_rec_i_G x y → In_rec_i_G x z → y = z.

Let Y and Z be given.

Assume H1: In_rec_i_G X Y.

Assume H2: In_rec_i_G X Z.

We will prove Y = Z.

We prove the intermediate claim L1: ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f.

An exact proof term for the current goal is (In_rec_i_G_inv X Y H1).

We prove the intermediate claim L2: ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Z = F X f.

An exact proof term for the current goal is (In_rec_i_G_inv X Z H2).

Apply (exandE_ii (λf ⇒ ∀x ∈ X, In_rec_i_G x (f x)) (λf ⇒ Y = F X f) L1) to the current goal.

Let g be given.

Assume H3: ∀x ∈ X, In_rec_i_G x (g x).

Assume H4: Y = F X g.

Apply (exandE_ii (λf ⇒ ∀x ∈ X, In_rec_i_G x (f x)) (λf ⇒ Z = F X f) L2) to the current goal.

Let h be given.

Assume H5: ∀x ∈ X, In_rec_i_G x (h x).

Assume H6: Z = F X h.

We will prove Y = Z.

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.

Assume H7: x ∈ X.

An exact proof term for the current goal is (IH x H7 (g x) (h x) (H3 x H7) (H5 x H7)).

∎