Let α, p and q be given.

Assume H1.

Let β be given.

Assume H2.

Apply iff_sym to the current goal.

An exact proof term for the current goal is H1 β H2.

∎