diff --git a/algebra/upred.v b/algebra/upred.v
index b4b5abe28c3bfa17941ed80355ff823d4a154b9a..18e438efbd7fbdc79badd47fce82c16d33bed91d 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1472,6 +1472,7 @@ Qed.
 
 Theorem soundness : ¬ (True ⊢ False).
 Proof. exact (adequacy False 0). Qed.
+
 End uPred_logic.
 
 (* Hint DB for the logic *)
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 68ce0feef788c5e06f1ed49dede0cb957caa2cb4..3e0504e93e40e4a1af2e70b5809c2ce413ff2ed7 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -269,10 +269,10 @@ Proof. by rewrite /MakeLater later_True. Qed.
 Global Instance make_later_default P : MakeLater P (â–· P) | 100.
 Proof. done. Qed.
 
-Global Instance frame_later R P Q Q' :
-  Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'.
+Global Instance frame_later R R' P Q Q' :
+  Frame R P Q → MakeLater Q Q' → IntoLater R' R → Frame R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
+  rewrite /Frame /MakeLater /IntoLater=><- <- ->. by rewrite later_sep.
 Qed.
 
 Class MakeExceptLast (P Q : uPred M) := make_except_last : ◇ P ⊣⊢ Q.