HepLean Documentation

Init.Data.PLift

instance instDecidableEqPLift {α✝ : Sort u_1} [DecidableEq α✝] :
Equations
  • instDecidableEqPLift = decEqPLift✝
Equations
  • =