fact: Definition mset_sat (φ : nat -> list nat) (l : list constraint) := Forall (fun '(A, B) => Permutation (mset_sem φ A) (mset_sem φ B)) l.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun