Why does my goal change?

Stream: new members

[Ali Sever]

After using constructor my goal was ?m_1 ∉ A. Then I used cases h with p hp, and my goal became ?m_1[_] ∉ A. What does that mean, and why does it even happen?

[Kenny Lau]

MWE

[Mario Carneiro]

That is a representation of a delayed abstraction. It means that the metavariable ?m_1 has been partially instantiated, although it still hasn't figured out what it should be yet

[Kevin Buzzard]

Ali I think it's an unwise idea in general to have metavariables in your goals. Presumably you have more than one goal at this point, and another goal is probably asking you what the metavariable is. You might want to fill in some earlier hole.