destruct <term>
replaces all occurrences of <term>
with a constructor applied to its arguments (which are generated as variables in the context), with one goal per constructor. With an evar, you can choose which constructor should be applied by doing the instantiation yourself, e.g. with instantiate (p := (?[p1], ?[p2])).