proposition: Fact fo_bisimilar_formula_vars : fol_vars ξ ⊑ 0::1::nil.
proof: Proof. unfold fo_bisimilar_formula; rewrite fol_vars_subst. intros n; rewrite in_flat_map; intros (? & _ & H). revert x H; intros [ | [] ]; simpl; tauto. 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)