proposition: Lemma filter2s_equiv p ps1 ps2 l1 l2 : tequiv ps1 ps2 -> lequiv l1 l2 -> tequiv (fold_left (filter2s p) l1 ps1) (fold_left (filter2s p) l2 ps2).
proof: Proof. intros (H1, (H2, H3)) H4. case (filter2s_correct p ps1 l1); intros Hr1 (Hs1, Ht1). case (filter2s_correct p ps2 l2); intros Hr2 (Hs2, Ht2). unfold lequiv in H1, H2, H3, H4; split; [idtac | split]; intros a; (rewrite Hr1; rewrite Hr2) || (rewrite Hs1; rewrite Hs2) || (rewrite Ht1; rewrite Ht2). - split; intros [HH | HH]. + rewrite <- H1; auto. + right; rewrite <- H2, <- H4; auto. + rewrite H1; auto. + right; rewrite H2, H4; auto. - split; intros [HH | HH]. + rewrite <- H2; auto. + right; rewrite <- H1, <- H4; auto. + rewrite H2; auto. + right; rewrite H1, H4; auto. - split; intros [HH | HH]. + rewrite <- H3; auto. + right; rewrite <- H1, <- H2, <- H4; auto. + rewrite H3; auto. + right; rewrite H1, H2, H4; auto. Qed.
imports: ZArith List