proposition: Theorem fo_model_nosyms : fol_sem M φ A <-> fol_sem M' φ A.
proof: Proof. Proof using HA H. apply fo_model_projection' with (ls := nil) (lr := fol_rels A) (i := fun x => x) (j := fun x => x); auto. + intros; rewrite H; auto. apply fol_equiv_ext; f_equal. apply vec_pos_ext; intro; rew vec. + rewrite HA; apply incl_refl. 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