Let α and p be given.

Apply PNoLeI2 to the current goal.

Apply PNoEq_ref_ to the current goal.

∎