proposition: Lemma in_in_map : forall (A B : Set) (f : A -> B) a l, In a l -> In (f a) (map f l).
proof: Proof. intros A B f a l; induction l as [ | b l ]; trivial. intro In_a; elim In_a; clear In_a; intro In_a. subst; left; trivial. right; apply IHl; trivial. Qed.
imports: List Arith