diff options
Diffstat (limited to 'theories/Sorting/Permutation.v')
| -rw-r--r-- | theories/Sorting/Permutation.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 65bf17ef0..cf9f8ee42 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -313,7 +313,7 @@ Qed. Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. Proof. intros a l H; remember [a] as m in H. - induction H; try (injection Heqm as -> ->; clear Heqm); + induction H; try (injection Heqm as -> ->); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed. |