Documentation
Init
.
Data
.
Prod
Search
Google site search
Init
.
Data
.
Prod
source
Imports
Init.SimpLemmas
Imported by
instLawfulBEqProdInstBEqProd
source
instance
instLawfulBEqProdInstBEqProd
{α :
Type
u_1}
{β :
Type
u_2}
[
BEq
α
]
[
BEq
β
]
[
LawfulBEq
α
]
[
LawfulBEq
β
]
:
LawfulBEq
(
α
×
β
)
Equations
@
instLawfulBEqProdInstBEqProd
=
@
instLawfulBEqProdInstBEqProd.proof_1