I am using a predicate pQuant that quantifies over two atoms from a signature C2 and states some property about them, using another predicate pProp(c2a,c2b).  The property is symmetric, that is, for every a1 and a2, pProp(a1,a2) is true iff pProp(a2,a1) is true.  

sig C1 {}
sig C2 {myC1s : set C1 }

fact pQuant { all c2a, c2b : C2 | pProp[c2a,c2b] }

pred pProp[c2a: C2, c2b: C2] {    c2a.myC1s = c2b.myC1s }

run {} for 40

In this small example, the fact that the property is symmetric is obvious.  In the general case, if it is not obvious, assume that I enforce it using another fact.

Rather than quantifying over all ordered pairs, it would suffice in this case to quantify over all unordered pairs.  From my understanding, this can make much difference in terms of the size of the generated CNF formula and the performance of the solver.

Is it possible to quantify over all unordered pairs?  If not, would this be considered a good candidate for a small new language feature?