proposition: Lemma eval_eq {p A B} : A ~p B -> eval p A = eval p B.
proof: Proof. elim: A B. { by move=> ? /Permutation_nil ->. } move=> a A IH B /[dup] /(Permutation_in a) /(_ (in_eq _ _)). move=> /(@in_split nat) [B1 [B2 ->]]. move=> /(@Permutation_cons_app_inv nat) /IH. rewrite /eval !map_app !list_sum_app /=. lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun