fact: Fixpoint fol_mquant q n (A : 𝔽) := match n with | 0 => A | S n => (fol_quant q) (fol_mquant q n A) end.
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