congr lemmas for ite/dite

Stream: lean4

[Gabriel Ebner]

I'm not sure if this is the right place to comment on this, but the old congr lemmas for ite/dite with the non-canonical decidability instance are coming back in https://github.com/leanprover/lean4/commit/c0f5ab1fa51bffaa571d47feb26a97d8b04b7d99
While these congruence lemmas look useful at first glance, they actually make the simplifier less powerful: simp can only prove ite p a b = ite p a b when the decidability instances in the two ites are definitionally equal (because eqSelf needs them to be).
A longer discussion is in lean#159, the PR removing these lemmas from the community edition.
In short, simp can't prove the following if iteCongr is added:

example (x : ℕ) : (if x > 3 ∧ true then 1 else 2) = (if x > 3 then 1 else 2) :=
by simp -- fails in Lean <= 3.7