proposition: Lemma incl_map A B (f : A -> B) l1 l2 : incl l1 l2 -> incl (map f l1) (map f l2).
proof: Proof. intros Hincl x Hinx. destruct (proj1 (in_map_iff _ _ _) Hinx) as [y [<- Hiny]]. now apply in_map, Hincl. Qed.
imports: PeanoNat