proposition: Theorem Σ11_discernable_dec_FSAT X Y : (forall u v : X, decidable (u ≢ v)) -> (forall u v : Y, decidable (u ≢ v)) -> forall A, decidable (FSAT (Σ11 X Y) A).
proof: Proof. intros H0 H1 A. destruct (Sig_discernable_dec_to_discrete H0 H1 A) as (DX & DY & ? & ? & ? & ? & B & HB); auto. destruct FSAT_FULL_MONADIC_DEC with (A := B); simpl; auto. + left; tauto. + right; tauto. Qed.
imports: List Arith Undecidability.Synthetic(Definitions ReducibilityFacts InformativeDefinitions InformativeReducibilityFacts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list 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 fo_sat_dec red_utils Sig_Sig_fin Sig_rem_props Sig_rem_constants Sig0 Sig1 Sig1_1 Sig_discernable)