diff options
| author | Hugo Herbelin | 2020-05-03 20:54:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-03 20:54:47 +0200 |
| commit | e4074cf4e9bc31616ec161541cb35a831573d384 (patch) | |
| tree | 8f84d2451c31b93bcc48bf83f3deb153a45ef9b7 | |
| parent | 3452a14b58ab88af686d3006b843bc064ab8f911 (diff) | |
| parent | 3b06585b1ab4c0e77afcdccf584335b7b8050697 (diff) | |
Merge PR #12238: [stdlib] [CPermutation] patch for #12031
Reviewed-by: herbelin
| -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]. |