proposition: Theorem FSAT_FULL_MONADIC_discernable A : decidable (FSAT Σ A).
proof: Proof. Proof using H4 H3 H2 H1. destruct (FSAT_FULL_MONADIC_FSAT_11 H3 H4) as (f & Hf). destruct (Σ11_discernable_dec_FSAT H1 H2 (f A)) as [ H | H ]. + left; apply Hf; auto. + right; contradict H; apply Hf; auto. 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)