Stream: Beginner Questions

Topic: Unfold only one occurrence

view this post on Zulip Julin Shaji (Feb 21 2025 at 05:07):

I have got a goal like this:

 1. (fst p โŠ— fst (๐Ÿญ, ๐Ÿญ), snd p โŠ— snd (๐Ÿญ, ๐Ÿญ)) = p

Is there a way to unfold only the second fst?

view this post on Zulip Mathias Fleury (Feb 21 2025 at 05:31):

apply (subst thm) or even apply (subst (1) thm) (or any other number representing the occurrence in the formula). Needs (asm) for unfolding in assumptions

Last updated: Nov 13 2025 at 04:27 UTC