diff --git a/algebra/cofe.v b/algebra/cofe.v
index 0d35a88a0c3a5fc67aee6593afe105612c432a05..9742a09158804010373d7f6640faf3f7f60b3ae5 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -675,8 +675,6 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
-Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
-Proof. by destruct x. Qed.
 
 Section later.
   Context {A : cofeT}.
diff --git a/algebra/upred.v b/algebra/upred.v
index 37cc9c626a24d14998c45c601c19f6aba8cf5c52..781094a6032aa4d02415c6f2a893dce6f94f58ec 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1213,8 +1213,7 @@ Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 
 (* Later *)
-Lemma later_equivI {A : cofeT} (x y : later A) :
-  x ≡ y ⊣⊢ ▷ (later_car x ≡ later_car y).
+Lemma later_equivI {A : cofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. by unseal. Qed.
 
 (* Discrete *)
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index ad1ae6176d518c8971b2e7bc352dffb408dc0386..f59c7af6fe158f124e9987a945d40f7d0ee7c92b 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -126,7 +126,7 @@ Proof.
     iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
     iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
   rewrite /invariant_unfold.
-  by rewrite agree_equivI uPred.later_equivI /= iProp_unfold_equivI.
+  by rewrite agree_equivI uPred.later_equivI iProp_unfold_equivI.
 Qed.
 
 Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 0874a7e9ff2de0553cb18c4ad2585057f2613c55..ecfe85db26e1a289c7ba5fdc941f23424ae3141a 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -35,7 +35,7 @@ Section saved_prop.
   Lemma saved_prop_agree γ x y :
     saved_prop_own γ x ★ saved_prop_own γ y ⊢ ▷ (x ≡ y).
   Proof.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI /=.
+    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.