[Merged by Bors] - chore: fix implicit-reducible diamonds in Primrec#38305
Closed
sgouezel wants to merge 1 commit intoleanprover-community:masterfrom
Closed
[Merged by Bors] - chore: fix implicit-reducible diamonds in Primrec#38305sgouezel wants to merge 1 commit intoleanprover-community:masterfrom
sgouezel wants to merge 1 commit intoleanprover-community:masterfrom
