proposition: Fact fo_bisimilar_formula_sem φ x y : M,y·x·φ ⊨ ξ <-> x ≐ y.
proof: Proof. unfold fo_bisimilar_formula; rewrite fol_sem_subst. apply (proj2_sig fo_bisimilar_fol_def). Qed.
imports: List Arith Nat Lia Relations Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations decidable gfp fol_ops fo_sig fo_terms fo_logic fo_definable fo_sat)