proposition: Fact fo_bisimilar_formula_syms : fol_syms ξ ⊑ ls.
proof: Proof. unfold fo_bisimilar_formula; red. apply Forall_forall, fol_syms_subst. + intros [ | []]; rew fot; auto. + apply Forall_forall, (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)