I was wondering, whether it would be a good idea to generalize the library to arbitrary setoids. I'm currently using Autosubst for a inductive type with dependent type constructors. Because of this, I'm not using the standard Leibniz equality [eq] very often.
The standard library also offers eq_setoid. By this, the current use case should easily work as this would be the standard Instance most of the time.
I was wondering, whether it would be a good idea to generalize the library to arbitrary setoids. I'm currently using Autosubst for a inductive type with dependent type constructors. Because of this, I'm not using the standard Leibniz equality [eq] very often.
The standard library also offers
eq_setoid. By this, the current use case should easily work as this would be the standard Instance most of the time.