proposition: Lemma appears_filter x l f : appears x l = false -> appears x (filter f l) = false.
proof: Proof. induction l. reflexivity. simpl. destruct (f a); simpl; destruct (x =? a); auto. discriminate. Qed.
imports: Arith ZArith List Lia