proposition: Fact fot_def_ext t : fot_definable t -> forall φ ψ, (forall n, φ n = ψ n) -> t φ = t ψ.
proof: Proof. intros (k & _ & Hk) phi psi H. rewrite <- Hk, <- Hk; apply fo_term_sem_ext; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)