Roger Bosman (May 05 2021 at 10:33): Roger Bosman (May 05 2021 at 10:33):Hi all, 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?
MackieLoeffel (May 05 2021 at 12:04):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: Apr 19 2024 at 08:01 UTC