diff --git a/Kami/Lib/DepEq.v b/Kami/Lib/DepEq.v
index 65dcce5..3bd58fc 100644
--- a/Kami/Lib/DepEq.v
+++ b/Kami/Lib/DepEq.v
@@ -24,7 +24,8 @@ Ltac generalize_proof :=
     end.
 
 Ltac eq_rect_simpl :=
-  unfold eq_rec_r, eq_rec;
+  unfold eq_rec_r;
+  change eq_rec with (fun A x (P:A -> Set) => @eq_rect A x P);
   repeat rewrite eq_rect_nat_double;
   repeat rewrite <- (eq_rect_eq_dec Nat.eq_dec).
 
diff --git a/Kami/Lib/Word.v b/Kami/Lib/Word.v
index e68207a..b194ce5 100644
--- a/Kami/Lib/Word.v
+++ b/Kami/Lib/Word.v
@@ -3934,7 +3934,7 @@ Lemma wrshifta_0:
   forall sz (w: word sz), wrshifta w 0 = w.
 Proof.
   unfold wrshifta; intros; simpl.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   unfold sext.
   destruct (wmsb w false).
   - cbn; rewrite combine_n_0.
@@ -3947,7 +3947,7 @@ Lemma wrshifta_WO:
   forall n, wrshifta WO n = WO.
 Proof.
   unfold wrshifta; cbn; intros.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite wzero_eq_rect.
   rewrite <-combine_wzero.
   rewrite split2_combine.
@@ -3974,7 +3974,7 @@ Proof.
   intros.
   unfold wrshifta; cbn.
   rewrite sext_wzero.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite wzero_eq_rect.
   rewrite <-combine_wzero.
   rewrite split2_combine.
@@ -4250,7 +4250,7 @@ Lemma wordToNat_wrshifta:
 Proof.
   unfold wrshifta; intros.
   rewrite wordToNat_split2.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite wordToNat_eq_rect.
   reflexivity.
 Qed.
@@ -4287,7 +4287,7 @@ Proof.
   
   - unfold wlshift; intros.
     rewrite wordToNat_split1.
-    unfold eq_rec_r, eq_rec.
+    eq_rect_simpl.
     rewrite wordToNat_eq_rect.
     rewrite wordToNat_combine.
     rewrite wordToNat_wzero; simpl.
@@ -6743,7 +6743,7 @@ Proof.
   apply wordToNat_inj.
   unfold wlshift.
   rewrite? wordToNat_split1.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite? wordToNat_eq_rect.
   rewrite? wordToNat_combine.
   rewrite? wordToNat_wzero.
@@ -6792,7 +6792,7 @@ Proof.
   apply wordToNat_inj.
   unfold wlshift.
   rewrite? wordToNat_split1.
-  unfold eq_rec_r, eq_rec.
+  eq_rect_simpl.
   rewrite? wordToNat_eq_rect.
   rewrite? wordToNat_combine.
   rewrite? wordToNat_wzero.