Documentation
Iris
.
Std
.
Equivalence
Search
return to top
source
Imports
Init
Imported by
equivalence_eq
source
theorem
equivalence_eq
{
α
:
Sort
u_1}
:
Equivalence
Eq