proposition: Lemma soundness {l} : LPolyNC_SAT (map encode_msetc l) -> FMsetC_SAT l.
proof: Proof. have eq_trans A B C : A ≡ B -> B ≡ C -> A ≡ C. { move=> H1 H2 c. by rewrite (H1 c) (H2 c). } move=> [ψ]. rewrite -Forall_forall Forall_map => Hψ. exists (fun x => poly_to_mset (ψ x)). rewrite -Forall_forall. apply: Forall_impl; last by eassumption. case. - by move=> x /= /poly_to_mset_eqI. - move=> x y z /= /poly_to_mset_eqI. move /eq_trans. apply. by apply: poly_to_mset_addP. - move=> x y /= /poly_to_mset_eqI. move /eq_trans. apply. move: (ψ y) => p. rewrite -poly_to_mset_consP. apply: poly_to_mset_eqI. by apply: poly_shiftI. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun