Stream: Beginner Questions

Topic: Unfold only one occurrence

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?

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: Jan 17 2026 at 20:25 UTC