proposition: Lemma list_prop_reduced_list: forall {A : Type} (Q : A -> Prop) (Q_lem : forall a, Q a \/ ~Q a) (l : list A), exists l', forall a, In a l' <-> (In a l /\ Q a).
proof: Proof. induction l. exists nil. split; inversion 1. trivial. destruct IHl as [l' ?]. simpl. destruct (Q_lem a). exists (a :: l'). simpl. split; intros. destruct H1. subst a0. split; auto. rewrite H in H1. tauto. destruct H1. destruct H1. auto. right. rewrite H. tauto. exists l'. split; intros. rewrite H in H1. tauto. destruct H1. destruct H1. subst. contradiction. rewrite H. 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