Commit 2025-11-18 14:10 a14e51d4

feat(contrapose): cancel negations, and support ↔ (#31510) This PR introduces two features for contrapose:

• contrapose applied to a goal p ↔ q creates the goal ¬p ↔ ¬q.
• Instead of creating double negations, contrapose will try to cancel out double negations that it creates. This will allow for replacing some occurrences of contrapose! with contrapose (TODO: write a linter for this?). It also allows avoiding classical logic in some cases. Zulip discussion