proposition: Lemma encode_constraint_sat {φ x y z} : 1 + (φ x) + (φ y) * (φ y) = (φ z) -> mset_sat (construct_valuation φ) (encode_constraint x y z).
proof: Proof. move=> Hxyz. rewrite /encode_constraint /mset_sat ?Forall_app -?/(mset_sat _ _). do 3 (constructor; first by apply: encode_bound_sat). do 3 (constructor; first by apply: encode_nat_sat). constructor; last done. rewrite /mset_sem /construct_valuation ? embed_unembed. have ->: [0] = repeat 0 1 by done. rewrite -?repeat_app. apply: Permutation_refl'. congr repeat. move: Hxyz=> <-. clear. elim: (φ y); clear; first by (move=> /=; lia). move=> φy IH. rewrite /pyramid seq_last /(plus 0 _) flat_map_concat_map map_app concat_app. rewrite -flat_map_concat_map -/(pyramid _) /= ?app_length seq_length /=. by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun