proposition: Lemma perm_trans : transitive _ perm.
proof: Proof. intros l l' l'' H; generalize l''. induction H as [|l0 l'0 H0 IHperm]. - trivial. - intros l''0 H2; apply IHperm; eapply perm_intro_r; eauto. Qed.
imports: List Relations