Let alpha, p and q be given.

Assume H1.

Let beta be given.

Assume H2.

Apply iff_sym to the current goal.

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

∎