Commit 2024-05-15 13:09 600a5fa3
View on Github →feat: port cc
tactic (2/3) (#11960)
In this PR, we implements process when an new equation is added to a congruence closure.
Also, Lean.Expr.relSidesIfSymm?
is removed in #11162, but this def is required for cc
tactic, so we recover this.