Commit 2025-05-24 17:56 ecc639e1

View on Github →

chore: remove erw from Sym2.other_spec (#25158) This PR addresses an erw linter instance by rewriting a proof.

Estimated changes

modified theorem Sym2.other_spec