proposition: Theorem fo_fin_model_discretize : { n : nat & { Md : fo_model Σ (pos n) & { _ : fo_model_dec Md & { _ : fo_projection ls lr M Md & (forall p q, fo_bisimilar Md p q <-> p = q) } } } }.
proof: Proof. Proof using E1. exists n, Md. exists; eauto. red; simpl; auto. 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)