proposition: Lemma encode_nat_sat {φ x} : mset_sat (construct_valuation φ) (encode_nat x).
proof: Proof. rewrite /encode_nat /mset_sat !Forall_cons_iff Forall_nil_iff /mset_sem /construct_valuation ?embed_unembed. rewrite -?repeat_app. constructor. { apply: Permutation_refl'. congr repeat. have := pyramid_length (φ x). by lia. } constructor. { apply: Permutation_refl'. congr repeat. have := pyramid_length (φ x). by lia. } constructor; first by apply: seq_sat1. constructor; first by apply: pyramid_shuffle. constructor; last done. by apply: encode_nat_sat_aux. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun