proposition: Lemma soundness {l} : FMsetC_SAT (encode_problem l) -> FMsetTC_SAT l.
proof: Proof. move=> [ψ]. rewrite -Forall_forall Forall_flat_map => Hψ. pose φ x := ψ (term_to_nat (mset_term_var x)). exists φ. apply: Forall_impl; last by eassumption. move=> [t u] /Forall_app [/Forall_cons_iff [+] /Forall_cons_iff [+ _]] /Forall_app [] => /=. move=> /Permutation_count_occ /(Permutation_app_inv_r _ []) /Permutation_nil -> /=. move=> /Permutation_count_occ Hψtu. have Hφ (s) : Forall (msetc_sem ψ) (term_to_msetcs s) -> Permutation (mset_sem φ s) (ψ (term_to_nat s)). { clear. elim: s. - by move=> /Forall_cons_iff /= [] /Permutation_count_occ ->. - done. - move=> t IHt u IHu /= /Forall_cons_iff /= [/Permutation_count_occ ->]. by move=> /Forall_app [/IHt -> /IHu ->]. - move=> t IH /= /Forall_cons_iff /= [/Permutation_count_occ ->]. by move=> /IH /Permutation_map. } by move=> /Hφ -> /Hφ ->. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun