proposition: Theorem fol_uniformize_complete A φ : incl (fol_rels A) lr -> fol_sem M φ A <-> fol_sem M' φ (fol_uniformize A).
proof: Proof. Proof using Hlr. revert φ; induction A as [ | r v | b A HA B HB | q A HA ]; simpl; try tauto; intros phi Hr. + rewrite vec_map_fill_tail; rew fot. apply Hlr, Hr; simpl; auto. + apply fol_bin_sem_ext; auto. * apply HA; intros ? ?; apply Hr, in_app_iff; auto. * apply HB; intros ? ?; apply Hr, in_app_iff; 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)