Even if not symmetrical in both sets, it is surely symmetrical in {<<a, x>>, <<b, y>>, <<c, z>>}, because the original model (just `foo`) is symmetrical in {x, y, z}, no? Perhaps TLC should provide a way to specify this symmetry (e.g. with a predicate on composed permutations)?