proposition: Lemma encode_bound_sat {φ x} : mset_sat (construct_valuation φ) (encode_bound x).
proof: Proof. rewrite /encode_bound /mset_sat !Forall_cons_iff Forall_nil_iff /mset_sem. rewrite /construct_valuation ? embed_unembed. pose A d n := map (fun i => (S d) * i) (seq 0 n). constructor; first by apply: seq_sat1. constructor. { have -> (X) : map S (map S X) = map (fun i => 2+i) X by rewrite map_map. by apply: seq_sat2. } constructor; first by apply: proj2_sig (unify_sat _). constructor. { have -> (n): [n] = [1*n] by rewrite Nat.mul_1_l. by apply: nat_sat. } constructor; [|done]. rewrite map_map. by apply: nat_sat. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun