proposition: Lemma Permutation_transp_cons : forall (x : A) l1 l2, Permutation_transp l1 l2 -> Permutation_transp (x :: l1) (x :: l2).
proof: Proof. intros x l1 l2 HP. induction HP. - reflexivity. - rewrite 2 app_comm_cons. apply perm_t_swap. - now transitivity (x :: l'). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat