proposition: Theorem CPermutation_nil_app_cons : forall l1 l2 a, ~ CPermutation [] (l1 ++ a ::l2).
proof: Proof. intros l1 l2 a HC; apply CPermutation_nil in HC; destruct l1; inversion HC. Qed.
imports: List Permutation Morphisms PeanoNat