proposition: Lemma permut_impl : forall (A B : Type) (R R' : A -> B -> Prop) l1 l2, (forall a b, R a b -> R' a b) -> permut0 R l1 l2 -> permut0 R' l1 l2.
proof: Proof. intros A B R R' l1; induction l1 as [ | a1 l1]; intros l2 Compat P; inversion P as [ | a b k k1 k2 a_R_b Q]; subst. apply Pnil. apply Pcons. apply Compat; trivial. apply IHl1; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)