Let alpha, p and beta be given.

Assume H2.

Apply iff_refl to the current goal.

∎