proposition: Theorem list_dec l : { x | In x l /\ P x } + { forall x, In x l -> Q x }.
proof: Proof. Proof using H. induction l as [ | x l IHl ]. + right; intros _ []. + destruct (H x) as [ Hx | Hx ]. 1: { left; exists x; simpl; auto. } destruct IHl as [ (y & H1 & H2) | H1 ]. * left; exists y; split; auto; right; auto. * right; intros ? [ -> | ? ]; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)