proposition: Lemma filters_equiv ps1 ps2 l1 l2 : pequiv ps1 ps2 -> lequiv l1 l2 -> pequiv (fold_left filters l1 ps1) (fold_left filters l2 ps2).
proof: Proof. intros (H1, H2) H3. case (filters_correct ps1 l1); intros Hr1 Hs1. case (filters_correct ps2 l2); intros Hr2 Hs2. split; intros a; (rewrite Hr1; rewrite Hr2) ||(rewrite Hs1; rewrite Hs2). - unfold lequiv in H1, H3; rewrite H1, H3; split; auto. - unfold lequiv in H1, H2, H3; rewrite H1, H2, H3; split; auto. Qed.
imports: ZArith List