Is there a variant of `simp` that handles reverse simps?

Stream: new members

[Abhimanyu Pallavi Sudhir]

Is there a variant of simp so I can write things like simp [←P, Q] or simp only [←P, Q] where P and Q may or may not be simp lemmas?

[Kenny Lau]

nope. you need to do P.symm

[Mario Carneiro]

and you alsso need to remove P if it is a simp lemma or it will go into a loop

[Chris Hughes]

remove P, means do simp [P.symm, -P]

[Mario Carneiro]

maybe we should write simp'? I'm sure this isn't the last tweak we will want