proposition: Lemma permut_rev : forall (A B : Type) (R : A -> B -> Prop) l1 l2, permut0 R l1 l2 -> permut0 (fun b a => R a b) l2 l1.
proof: Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l2 P; inversion P as [ | a b l1' l2' l2'' a_R_b Q]; subst. apply Pnil. apply (@permut_strong B A (fun b a => R a b) b a1 l2' l2'' (@nil _) l1); trivial. simpl; apply IHl1; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)