proposition: Lemma rel_map_map_inv : forall (A B C : Type)(rel : B -> C -> Prop)(f : A -> B)(lsa : list A)(lsc : list C), rel_map rel (map f lsa) lsc -> rel_map (fun a c => rel (f a) c) lsa lsc.
proof: Proof. induction lsa; intuition; simpl in *. inversion H; subst; clear H. econstructor. inversion H; clear H; subst. econstructor. eapply IHlsa; eauto. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation