proposition: Theorem rel_map_map2 : forall (A B C D : Type)(ls_c : list C)(ls_d: list D)(P : A -> B -> Prop)(f1 : C -> A)(f2 : D -> B), rel_map (fun a b => P (f1 a) (f2 b)) ls_c ls_d -> rel_map P (map f1 ls_c) (map f2 ls_d).
proof: Proof. induction ls_c; intuition. inversion H; subst. simpl. econstructor. inversion H; clear H; subst. simpl. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation