Instances on pempty #
This file collects facts about algebraic structures on the (universe-polymorphic) empty type, e.g. that it is a semigroup.
theorem
AddSemigroupPEmpty.proof_1
(x : PEmpty.{u_1 + 1} )
(y : PEmpty.{u_1 + 1} )
(z : PEmpty.{u_1 + 1} )
: