proposition: Lemma filter_ext: forall {A} (f g: A -> bool) l, (forall i, In i l -> f i = g i) -> filter f l = filter g l.
proof: Proof. intros. induction l; simpl. 1: reflexivity. assert (f a = g a) by (apply H; left; reflexivity). assert (forall i : A, In i l -> f i = g i) by (intros; apply H; right; assumption). destruct (f a), (g a); [|inversion H0.. |]; rewrite IHl by assumption; reflexivity. 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