Commit 2023-11-16 23:07 79da87bb

fix: remove references to non-heterogenous operators in theorem statements (#8086) Some of these are likely porting errors. Statements should always be about the heterogenous versions because these are the ones with notation. For places where we are abusing defeq, this debuts the trick of using (by exact a : B) = (by exact a1) + (by exact b2) to ensure the = and + are typed as B instead of A.