diff options
Diffstat (limited to 'theories/Lists/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 0e56a96bd..e82277a45 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -762,7 +762,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. repeat red. intros. -rewrite (app_nil_end (rev x)), (app_nil_end (rev y)). +rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. |