proposition: Lemma filter_sum_left_In_iff {A B}: forall e (l: list (A + B)), In (inl e) l <-> In e (filter_sum_left l).
proof: Proof. intros. induction l; simpl; intuition. - inversion H2. simpl. left; reflexivity. - simpl in H1. destruct H1. + subst a0. left; reflexivity. + right. apply H0. assumption. - inversion H2. 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