Let p and q be given.

Assume H1 H2.

Apply prop_ext to the current goal.

Apply iffI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

∎