proposition: Theorem fo_model_projection' A : (forall n, n ∊ fol_vars A -> i (φ n) = ψ n) -> fol_syms A ⊑ ls -> fol_rels A ⊑ lr -> fol_sem M φ A <-> fol_sem N ψ A.
proof: Proof. Proof using Hs Hr E. apply fo_model_projection with (p := p). 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