Let α, p and β be given.

Assume H2.

Apply iff_refl to the current goal.

∎