proposition: Fact fot_def_equiv f g : (forall φ, f φ = g φ) -> fot_definable f -> fot_definable g.
proof: Proof. intros E (t & H1 & H2); exists t; split; auto; intro; rewrite H2; 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)