Assume H1.

Apply func_ext set (set → set) to the current goal.

Let x be given.

Apply func_ext set set to the current goal.

Let y be given.

We will prove If_iii x y = f x y.

An exact proof term for the current goal is If_i_1 p (f x y) (g x y) H1.

∎