- When using generalized rewriting, can I get
`rewrite H`

with`H : f ≡ g`

to rewrite`f x ≡ t`

to`g x ≡ t`

? - If that’s not possible (as it seems), are there plans to make it possible?

I already know this doesn’t work in `coq-stdpp`

and Iris, so one uses other tactics (here, usually, `repeat f_equiv; apply H`

), tho they have their limitations; but I don’t even know how to google for this problem, let alone find any discussion or plans to address this.

To rewrite `f x ≡ f y`

given `x ≡ y`

I must declare that `f`

is a `Proper`

morphism for `≡`

, but here it seems I’d need a way to declare that the builtin “function application operator” is `Proper`

for `≡`

— which makes little sense.

It seems you’d need a way to declare that `≡`

itself is a congruence for application, by proving that

`∀ f g : A → B, f ≡ g → ∀ x, f x ≡ g x`

. Which can be ensured, for instance, by using a setoid on functions that validates extensionality:

```
Instance fun_equiv `{Equiv B} : Equiv (A → B) := λ f g, ∀ x, f x ≡ g x.
```