proposition: Lemma or_dec_prop_list_split: forall {A} (l: list A) P Q, NoDup l -> (forall x, Decidable (P x)) -> (forall x, Decidable (Q x)) -> (forall x, In x l <-> P x \/ Q x) -> exists lp lq, NoDup lp /\ NoDup lq /\ (forall x, In x lp <-> P x) /\ (forall x, In x lq <-> Q x) /\ (forall x, In x l <-> In x lp \/ In x lq).
proof: Proof. intros. exists (select X l), (select X0 l). split5; intros. + apply NoDup_select; auto. + apply NoDup_select; auto. + rewrite select_In. firstorder. + rewrite select_In. firstorder. + do 2 rewrite select_In. firstorder. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver