instance instDecidableEqULift {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ULift α✝)

Equations

• instDecidableEqULift = decEqULift✝

theorem instSubsingletonULift {α : Type u_1} [Subsingleton α] : Subsingleton (ULift α)