Require Import List Arith Lia.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list finite.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.TRAKHTENBROT
Require Import notations fol_ops fo_sig fo_terms fo_logic fo_sat discrete.
Set Implicit Arguments.
Theorem fo_discrete_removal Σ (A : fol_form Σ) :
fo_form_fin_dec_SAT A
-> exists n, fo_form_fin_discr_dec_SAT_in A (pos n).
Proof.
intros (X & M & Hfin & Hdec & phi & HA).
set (ls := fol_syms A).
set (lr := fol_rels A).
destruct (fo_fin_model_discretize ls lr Hfin Hdec)
as (n & Md & Mdec & f & E).
set (psy n := f (phi n)).
exists n, (@pos_eq_dec _), Md, (finite_t_pos _) , Mdec, psy.
revert HA.
apply fo_model_projection with (p := f);
unfold lr, ls; auto; apply incl_refl.
Qed.
Theorem fo_form_fin_dec_SAT_fin_discr_dec Σ (A : fol_form Σ) :
fo_form_fin_dec_SAT A
-> fo_form_fin_discr_dec_SAT A.
Proof.
intros H.
destruct fo_discrete_removal with (1 := H) (A := A)
as (n & Hn); auto.
exists (pos n); auto.
Qed.