proposition: Corollary btm_fa_dec (P : _ -> Prop) t : (forall s t, s ≈ t -> P s -> P t) -> (forall x, x ∈ t -> { P x } + { ~ P x }) -> { s | s ∈ t /\ ~ P s } + { forall s, s ∈ t -> P s }.
proof: Proof. intros H1 H2. destruct btm_ex_dec with (P := fun x => ~ P x) (t := t) as [ H | H ]; auto. + intros u v G1 G2; contradict G2; revert G2; apply H1; auto. + intros x Hx; specialize (H2 _ Hx); tauto. + right; intros s Hs; specialize (H _ Hs). destruct (H2 _ Hs); tauto. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite seteq) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops)