Commit 2020-12-01 23:23 9a4ed2aa

refactor(*): Add _injective alongside _inj lemmas (#5150) This adds four new injective lemmas:

• list.append_right_injective
• list.append_left_injective
• sub_right_injective
• sub_left_injective It also replaces as many *_inj lemmas as possible with an implementation of *_injective.eq_iff, to make it clear that the lemmas are just aliases of each other.