instance instDecidableEqPLift {α✝ : Sort u_1} [DecidableEq α✝] : DecidableEq (PLift α✝)

theorem instSubsingletonPLift {α : Sort u_1} [Subsingleton α] : Subsingleton (PLift α)