proposition: Lemma collision_filter l f : collision l = false -> collision (filter f l) = false.
proof: Proof. induction l. reflexivity. simpl. destruct (appears a l) eqn:E1. discriminate. intros E2. destruct (f a). simpl in *. rewrite appears_filter; auto. auto. Qed.
imports: Arith ZArith List Lia