Suppose I have a goal with subterm t. I want to simplify or unfold something, say the induction principle for a sum `sum_ind`

only within t without affecting the rest of the goal. How can I do this?

The way I had set up was something like

```
let X := fresh "var" in
set (X := t) ; unfold sum_ind in X; unfold X
```

but this doesn't work when there are bound variables in t so that the subterm can't be extracted or generalized.

if you want to simplify/rewrite in subterms, you may want to try SSReflect (can be used without MathComp). There was a whole paper on subterm selection...

```
rewrite [in t]/sum_ind
```

should do it (once you require `ssreflect`

)

Last updated: Sep 30 2023 at 06:01 UTC