proposition: Lemma list_decidable_prop_reduced_list: forall {A : Type} (P Q : A -> Prop) (l: list A), (forall a, Q a \/ ~Q a) -> (forall a, In a l <-> P a) -> (exists l', (forall a, In a l' <-> P a /\ Q a)).
proof: Proof. intros. destruct (list_prop_reduced_list Q H l) as [l' ?]. exists l'. intuition. apply H1 in H2. destruct H2. apply H0. trivial. apply H1 in H2. tauto. apply H0 in H3. apply H1. tauto. 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