proposition: Lemma permut_map : forall (A B A' B': Type) (R : A -> B -> Prop) (R' : A' -> B' -> Prop) (f1 : A -> A') (f2 : B -> B') l1 l2, (forall a b, In a l1 -> In b l2 -> R a b -> R' (f1 a) (f2 b)) -> permut0 R l1 l2 -> permut0 R' (map f1 l1) (map f2 l2).
proof: Proof. intros A B A' B' R R' f1 f2 l1; induction l1 as [ | a1 l1]; intros l2 Compat P; inversion P as [ | a' b l1' l2' l2'' a_R_b P' H]; subst. simpl; apply Pnil. rewrite map_app; simpl; apply Pcons. apply Compat; trivial. left; trivial. apply in_or_app; right; left; trivial. rewrite <- map_app; apply IHl1; trivial. intros a b' a_in_l1 b'_in_l2; apply Compat. right; trivial. apply in_insert; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)