lean4
lean4 copied to clipboard
Congruence closure and e-matching
Lean 3 has this feature. It has performance problems and limitations.