I want to simplify only the arguments of a specific constructor. Maybe one can do this using `pattern_occs`

but I can't figure out the syntax.

E.g. how would I simplify only the argument of the `S`

, but not the right hand side in:

```
Goal forall a:nat, S (0 + a) = 0 + a.
intros a.
```

`reference_occs`

btw. only works for function calls, not for constructors.

`rewrite [S _]/=`

with ssreflect rewrite should work?

Last updated: Feb 06 2023 at 13:03 UTC