Grind extensionality attribute to mark which [ext]
theorems should be used.
@[reducible, inline]
Extensionality theorems that can be used by grind
Grind extensionality attribute to mark which [ext]
theorems should be used.
Extensionality theorems that can be used by grind