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
Last updated: Sep 30 2023 at 06:01 UTC