fact: Definition encode_bound_spec {φ x} : mset_sat φ (encode_bound x) -> Forall (fun a => 0 = a) (φ (embed (x, 0, 0))).
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun