proposition: Lemma encode_constraint_spec {φ x y z} : mset_sat φ (encode_constraint x y z) -> 1 + length (φ (embed (x, 0, 1))) + length(φ (embed (y, 0, 1))) * length(φ (embed (y, 0, 1))) = length(φ (embed (z, 0, 1))).
proof: Proof. rewrite /encode_constraint /mset_sat ?Forall_app -?/(mset_sat _ _). move=> [Hx [Hy [Hz]]]. move=> [/(encode_nat_spec Hx) ? [/(encode_nat_spec Hy) ? [/(encode_nat_spec Hz) ?]]]. rewrite /mset_sat Forall_cons_iff Forall_nil_iff /mset_sem. move=> [/Permutation_length]. rewrite ? app_length /=. by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun