proposition: Lemma rel_map_app_inv : forall (A B : Type)(rel : A -> B -> Prop)(lsa1 lsa2 : list A)(lsb : list B), rel_map rel (lsa1 ++ lsa2) lsb -> (rel_map rel lsa1 (firstn (length lsa1) lsb) /\ rel_map rel lsa2 (skipn (length lsa1) lsb)).
proof: Proof. induction lsa1; intuition; simpl in *. econstructor. inversion H; clear H; subst. econstructor. eapply IHlsa1; eauto. trivial. inversion H; clear H; subst. eapply IHlsa1; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation