proposition: Lemma Permutation_Permutation_transp : forall l1 l2 : list A, Permutation l1 l2 <-> Permutation_transp l1 l2.
proof: Proof. intros l1 l2; split; intros HP; induction HP; intuition auto. - solve_relation. - now apply Permutation_transp_cons. - rewrite <- (app_nil_l (y :: _)). rewrite <- (app_nil_l (x :: y :: _)). apply perm_t_swap. - now transitivity l'. - apply Permutation_app_head. apply perm_swap. - now transitivity l'. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat