proposition: Lemma CPermutation_length_2 : forall a1 a2 b1 b2, CPermutation [a1; a2] [b1; b2] -> a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
proof: Proof. intros; now apply Permutation_length_2, CPermutation_Permutation. Qed.
imports: List Permutation Morphisms PeanoNat