diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index 7714f3d59c5e42e6140cd8d72787e8984dead380..b766ed0d77332e8a0bba41d71fdec96423b1417f 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -231,7 +231,6 @@ Proof.
     inv H4. 
     assert (Some v1 = Some (Val.load_result (chunk_of_type ty) v')).
       rewrite <- LOAD1. eapply Mem.load_store_same; eauto.
-      replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
       destruct ty; auto.
     inv H4. rewrite load_result_ty; auto. 
     auto.