substs eliminates hypotheses of form
x = y by rewriting all occurances and then discharging the hypothesis. However, this does not work for alternate equivalence relations. Is there a setoid-based (?) variant that does this?
std++ has a
setoid_subst tactic that may do what you want (for the std++ equiv relation): https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v#L324
Last updated: Oct 03 2023 at 20:01 UTC