proposition: Lemma reduction_disc : @fo_form_fin_discr_dec_SAT (Σrel 2) ⪯ FSATd.
proof: Proof. exists translate. intros phi. split. - intros (D & HE & M & [L HL] & HD & rho & H). exists D, (@M1 D M), rho. repeat split. + exists L. apply HL. + apply discrete_iff. constructor. apply HE. + intros [ ]. apply decidable_iff. constructor. apply HD. + now apply fwd_sat. - intros (D & M & rho & [L HL] & [HE] % discrete_iff & HD & H). specialize (HD tt). apply decidable_iff in HD. destruct HD as [HD]. exists D, HE, (@M2 D M), (exist _ L HL). eexists. + intros []. apply HD. + exists rho. now apply bwd_sat. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.FOL.TRAKHTENBROT(fo_sat fo_sig fo_terms fo_logic fol_ops) Undecidability.Synthetic.DecidabilityFacts Vector Lia