proposition: Lemma completeness {l} : FMsetC_SAT l -> LPolyNC_SAT (map encode_msetc l).
proof: Proof. move=> [φ]. rewrite -Forall_forall => Hφ. exists (fun x => mset_to_poly (φ x)). rewrite -Forall_forall Forall_map. apply: Forall_impl; last by eassumption. case. - by move=> x /= /mset_to_poly_eqI. - move=> x y z /= /mset_to_poly_eqI + i => /(_ i) ->. by apply mset_to_poly_appP. - move=> x y /= /mset_to_poly_eqI + i => /(_ i) ->. move: (@poly_shiftI (mset_to_poly (φ y)) i) => /= ->. by apply: mset_to_poly_mapP. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun