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: Sep 23 2023 at 15:01 UTC