fact: Fixpoint fol_uniformize (A : fol_form Σ) : fol_form Σ' := match A with | ⊥ => ⊥ | @fol_atom _ r v => @fol_atom Σ' r (vec_fill_tail _ v (£0)) | fol_bin c A B => fol_bin c (fol_uniformize A) (fol_uniformize B) | fol_quant q A => fol_quant q (fol_uniformize A) end.
imports: List Arith Bool Lia Eqdep_dec 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 fo_logic fo_sat)