proposition: Theorem CPermutation_nil : forall l, CPermutation [] l -> l = [].
proof: Proof. intros l HC; inversion HC as [l1 l2 Heq]; subst. now apply app_eq_nil in Heq; destruct Heq; subst. Qed.
imports: List Permutation Morphisms PeanoNat