diff options
| author | Olivier Laurent | 2020-05-03 11:34:00 +0200 |
|---|---|---|
| committer | Olivier Laurent | 2020-05-03 11:34:00 +0200 |
| commit | 3b06585b1ab4c0e77afcdccf584335b7b8050697 (patch) | |
| tree | 99bbbca73a4aa46f7f55beed90f67b08cd6a8bc1 | |
| parent | f129326d545ae27d362132b279167d119894a992 (diff) | |
consistency with Permutation
| -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]. |