proposition: Fact fol_congruence_rels : fol_rels fol_congruence ⊑ lr.
proof: Proof. Proof using He. unfold fol_congruence. rewrite fol_rels_bin. apply incl_app. + apply fol_congruent_rels. + intros x Hx. apply fol_equivalence_rels in Hx. destruct Hx as [ | [] ]; subst; auto. Qed.
imports: List Arith Lia Relations 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 fo_logic) Undecidability.Shared.ListAutomation