Assume H1.

Apply func_ext set set to the current goal.

Let x be given.

We will prove If_ii x = f x.

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

∎