diff options
Diffstat (limited to 'theories/Sorting/PermutSetoid.v')
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 23ff22f92f..e973db4ad3 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -187,7 +187,7 @@ Qed. Lemma NoDupA_eqlistA_permut : forall l l', NoDupA eqA l -> NoDupA eqA l' -> - eqlistA eqA l l' -> permutation l l'. + equivlistA eqA l l' -> permutation l l'. Proof. intros. red; unfold meq; intros. |