proposition: Lemma permut_trans : forall (A : Type) (R : relation A) l1 l2 l3, (forall a b c, In a l1 -> In b l2 -> In c l3 -> R a b -> R b c -> R a c) -> permut0 R l1 l2 -> permut0 R l2 l3 -> permut0 R l1 l3.
proof: Proof. intros A R l1 l2; generalize l1; clear l1; induction l2 as [ | a2 l2]; intros l1 l3 trans_R P1 P2. inversion_clear P2; trivial. destruct (permut_inv_right P1) as [a1 [l1' [l1'' [a1_R_a2 [H Q1]]]]]; subst l1. inversion P2 as [ | a2' a3 l2' l3' l3'' a2_R_a3 Q2]; subst. apply permut_strong. apply trans_R with a2; trivial. apply in_or_app; right; left; trivial. left; trivial. apply in_or_app; right; left; trivial. apply IHl2; trivial. intros a b c; intros; apply trans_R with b; trivial. apply in_insert; trivial. right; trivial. apply in_insert; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)