proposition: Lemma permut0_trans : forall l1 l2 l3 : list A, permut0 eq_A l1 l2 -> permut0 eq_A l2 l3 -> permut0 eq_A l1 l3.
proof: Proof. intros l1 l2 l3 P1 P2; apply permut_trans with l2; trivial. intros a b c _ _ _ a_eq_b b_eq_c; transitivity b; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)