proposition: Fact finite_weak_dec X (P : X -> Prop) : finite X -> (forall x y : X, { x = y } + { x <> y }) -> (forall x, P x \/ ~ P x) -> inhabited (forall x, { P x } + { ~ P x }).
proof: Proof. intros H1 H2 H3. apply finite_fin_eq in H1. destruct fin_weak_dec with (Q := P) (2 := H1); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_decidable fin_base)