proposition: Fact fol_def_conj R T : fol_definable R -> fol_definable T -> fol_definable (fun φ => R φ /\ T φ).
proof: Proof. intros (A & H1 & H2 & H3) (B & HH4 & H5 & H6); exists (fol_bin fol_conj A B); msplit 2. 1,2: simpl; intro; rewrite in_app_iff; intros []; auto. intro; simpl; rewrite H3, H6; tauto. 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)