proposition: Lemma map_app : forall l1 l2, map f (l1 ++ l2) = (map f l1) ++ map f l2.
proof: Proof. induction l1; simpl; intros. refl. rewrite IHl1. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)