diff options
| -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 e973db4ad3..f262f5e400 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -185,7 +185,7 @@ Proof. destruct H2; apply eqA_trans with a; auto. Qed. -Lemma NoDupA_eqlistA_permut : +Lemma NoDupA_equivlistA_permut : forall l l', NoDupA eqA l -> NoDupA eqA l' -> equivlistA eqA l l' -> permutation l l'. Proof. |