I have to prove a number of theorems of the form (exists(a,b,c,...) : P(a,b,c,...)) => (exists(a,b,c,...) : Q(a,b,c,...)) where P=>Q is trivial once I get rid of the quantifications. The order of the quantified variables may not be the same in the two quantifications, but they have the same variables. Is there a way to tell PVS that it should instantiate "a" with "a!1", "b" with "b!1" etc.? -- Pertti