diff options
| -rw-r--r-- | theories/Sorting/CPermutation.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index fac9cd1d6d..21d04da877 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -154,7 +154,7 @@ Qed. Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b. Proof. intros; now apply Permutation_length_1, CPermutation_Permutation. Qed. -Lemma CPermutation_length_1_inv : forall l a, CPermutation [a] l -> l = [a]. +Lemma CPermutation_length_1_inv : forall a l, CPermutation [a] l -> l = [a]. Proof. intros; now apply Permutation_length_1_inv, CPermutation_Permutation. Qed. Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a]. |