proposition: Theorem list_choose_d l : (forall x, In x l -> P x \/ Q x) -> (exists x, In x l /\ P x) \/ forall x, In x l -> Q x.
proof: Proof. induction l as [ | x l IHl ]; intros Hl. + right; intros _ []. + destruct (Hl x) as [ H1 | H1 ]. * left; auto. * left; exists x; simpl; auto. * destruct IHl as [ (y & H2 & H3) | H2 ]. - intros; apply Hl; right; auto. - left; exists y; simpl; auto. - right; intros ? [ <- | ]; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list utils_nat)