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