Lemma duplication ite_self and ite_id

[nomeata]

We currently have both ite_self and ite_id which are both, up to argument order, identical.

There is more duplication between Init.SimpLemmas and Init.ByCases.

I’d say these lemmas are useful independent of simp and by_cases, and would suggest consolidating them in, say, a module Init.Ite dedicated to lemmas about ite and dite.

Versions

7dc1ceb

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.