proposition: Lemma rel_map_app : forall (A B : Type)(rel : A -> B -> Prop)(lsa1 lsa2 : list A)(lsb1 lsb2 : list B), rel_map rel lsa1 lsb1 -> rel_map rel lsa2 lsb2 -> rel_map rel (lsa1 ++ lsa2) (lsb1 ++ lsb2).
proof: Proof. induction lsa1; intuition; simpl in *. inversion H; clear H; subst. simpl. trivial. inversion H; clear H; subst. rewrite <- app_comm_cons. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation