proposition: Theorem FSAT_dec_implies_discernable_rels_dec (P Q : rels Σ) : decidable (discernable P Q).
proof: Proof. Proof using HXY. destruct (HXY (test P ⟑ (test Q ⤑ ⊥))) as [ H | H ]. + left; revert H; apply FSAT_equiv_discernable_rels. + right; contradict H; revert H; apply FSAT_equiv_discernable_rels. 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)