Let P and Q be given.

Assume H1.

Apply func_ext set prop to the current goal.

Let x be given.

Apply prop_ext to the current goal.

We will prove P x ↔ Q x.

An exact proof term for the current goal is H1 x.

∎