proposition: Theorem fol_uniformize_sound A φ : fol_sem M φ A <-> fol_sem M' φ (fol_uniformize A).
proof: Proof. revert φ; induction A as [ | r v | A HA B HB | q A HA ]; simpl; try tauto; intros phi. + apply fol_equiv_ext; f_equal. rewrite vec_map_fill_tail, vec_first_half_fill_tail; auto. + apply fol_bin_sem_ext; auto. + apply fol_quant_sem_ext; auto. Qed.
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)