proposition: Theorem Sig_discernable_dec_to_discrete X Y : (forall u v : X, decidable (u ≢ v)) -> (forall u v : Y, decidable (u ≢ v)) -> forall A : fol_form (Σ11 X Y), { DX : _ & { DY : _ & { _ : discrete DX & { _ : discrete DY & { _ : finite_t DX & { _ : finite_t DY & { B | FSAT (Σ11 X Y) A <-> FSAT (Σ11 DX DY) B } } } } } } }.
proof: Proof. intros HX HY A. generalize (discernable_discriminable_list HX (fol_syms A)) (discernable_discriminable_list HY (fol_rels A)); intros HlX HlY. destruct (@Σdiscriminable_discrete_correct _ _ _ HlX _ HlY A) as (DX & DY & ? & ? & ? & ? & B & HB). 1,2: apply incl_refl. exists DX, DY. do 4 (exists; [ auto | ]). exists B; auto. Qed.
imports: List Bool Undecidability.Synthetic(Definitions ReducibilityFacts InformativeDefinitions InformativeReducibilityFacts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable discernable fol_ops fo_sig fo_terms fo_logic fo_sat Sig1_1 red_utils)