proposition: Fact fin_weak_dec X (P Q : X -> Prop) : (forall x y : X, P x -> P y -> { x = y } + { x <> y } ) -> fin P -> (forall x, P x -> Q x \/ ~ Q x) -> inhabited (forall x, P x -> { Q x } + { ~ Q x }).
proof: Proof. intros H1 (l & Hl) H2. destruct (list_weak_dec l Q) as [ f ]. + intros; apply H1; apply Hl; auto. + intros; apply H2; apply Hl; auto. + exists; intros; apply f, Hl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_decidable fin_base)