proposition: Theorem FSAT_dec_implies_discernable_syms_dec (f g : syms Σ) : decidable (discernable f g).
proof: Proof. Proof using HXY HP. destruct (HXY (testt HP f ⟑ (testt HP g ⤑ ⊥))) as [ H | H ]. + left; revert H; apply FSAT_equiv_discernable_syms. + right; contradict H; revert H; apply FSAT_equiv_discernable_syms. 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)