diff options
Diffstat (limited to 'theories/Sorting/CPermutation.v')
| -rw-r--r-- | theories/Sorting/CPermutation.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index 21d04da877..31d9f7f0ed 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -235,9 +235,8 @@ induction m as [| b m]; intros l HC. apply CPermutation_nil in HC; inversion HC. - symmetry in HC. destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]]. - apply map_eq_app in Heq as [l1 [l1' [-> [-> Heq]]]]. - symmetry in Heq. - apply map_eq_cons in Heq as [a [l1'' [-> [-> ->]]]]. + apply map_eq_app in Heq as [l1 [l1' [-> [<- Heq]]]]. + apply map_eq_cons in Heq as [a [l1'' [-> [<- <-]]]]. exists (a :: l1'' ++ l1); split. + now simpl; rewrite map_app. + now rewrite app_comm_cons. |