proposition: Theorem fo_bisimilar_fol_def : fol_definable ls lr M (fun φ => φ 0 ≐ φ 1).
proof: Proof. Proof using fin dec. destruct fom_eq_finite as (n & Hn). apply fol_def_equiv with (R := fun φ => iter fom_op (fun _ _ : X => True) n (φ 0) (φ 1)). + intro; rewrite <- fom_eq_fol_characterization, <- Hn; tauto. + apply fol_def_iter_fom_op; 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)