You need to explicitly name existential variables (with the `?[x]`
syntax, e.g. `refine (?[A] ?[B])` if you want to be able to refer to
them by name later on, with instantiate, or with the named goal selector
`[x]: ` (see
Post by Jason Gross
You can instantiate them by number
instantiate (4 := B).Â instantiate (2 := A).Â This is not very
satisfying, but it works.
thanks for all the answers to my previous question.
FWIW, actually simpl seems to rewrite a goal without instantiating evars
given a goal
Â Î1 ++ l ++ A :: Î2 ++ B :: Î3 = ?Î1 ++ ?A :: ?Î2 ++ ?B :: ?Î3
how do I instantiate ?A to A and ?B to B?
instantiate (?A := A).
instantiate (A := A).
but both those produce error messages.