proposition: Fact fol_vars_mquant q n (A : 𝔽) : fol_vars (fol_mquant q n A) = flat_map (fun i => if le_lt_dec n i then (i-n::nil) else nil) (fol_vars A).
proof: Proof. revert A; induction n as [ | n IHn ]; intros A. + simpl; rewrite <- map_id at 1; rewrite <- flat_map_single. do 2 rewrite flat_map_concat_map; f_equal; apply map_ext. intro a; destruct (le_lt_dec 0 a); f_equal; lia. + rewrite fol_mquant_S. rewrite IHn; simpl fol_vars; rewrite flat_map_flat_map. do 2 rewrite flat_map_concat_map; f_equal; apply map_ext. intros [ | a ]; auto; simpl flat_map. rewrite app_nil_r. destruct (le_lt_dec n a); destruct (le_lt_dec (S n) (S a)); auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms) Undecidability.Shared.ListAutomation