Chengsong Tan (Nov 14 2023 at 18:46): Chengsong Tan (Nov 14 2023 at 18:46):What's the command for unfolding a definition in the conclusion, but leaving things unchanged in the premises? Say converting
[| P x; Q x' |] ==> P x' to [| P x; Q x' |] ==> P's_def x' .
Thanks a lot,
Chengsong
Jan van Brügge (Nov 14 2023 at 22:11):You can use subst, if you need to do it multiple times apply (subst thms)+
Chengsong Tan (Nov 15 2023 at 19:20):Jan van Brügge said:
You can use
subst, if you need to do it multiple timesapply (subst thms)+
Thank you, Jan!
Last updated: Nov 13 2025 at 04:27 UTC