Commit 2024-04-18 05:39 03939bbc
View on Github →chore: deprecate redundant theorems append_eq_cons_iff and cons_eq_append_iff (#11630)
These theorems already exist in Std:
https://github.com/leanprover/std4/blob/e5306c3b0edefe722370b7387ee9bcd4631d6c17/Std/Data/List/Lemmas.lean#L150-L157