proposition: Fact forall_list_sem_dec X (P : X -> Prop) (l : list X) : (forall x, { P x } + { ~ P x }) -> { forall x, In x l -> P x } + { ~ forall x, In x l -> P x }.
proof: Proof. intros H. destruct list_dec with (P := fun x => ~ P x) (Q := P) (l := l) as [ (x & H1 & H2) | H1 ]. + firstorder. + right; contradict H2; auto. + left; intros x; apply H1; auto. Qed.
imports: List Arith Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)