Commit 2024-09-11 05:42 4b83244f
View on Github →chore: deprecate dif_ctx_congr, move if_(ctx_)congr (#16692)
The few uses of dif_ctx_congr can all be replaced without increasing the line count. The other two ite congruence lemmas are moved to Logic.Basic.