fact: Definition FMsetTC_SAT (l: list constraint) := exists (φ : nat -> list nat), mset_sat φ l.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun