diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 3e0504e93e40e4a1af2e70b5809c2ce413ff2ed7..aba0e60c19acb10062295aa0ec48af5d65d25ffd 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -270,9 +270,9 @@ Global Instance make_later_default P : MakeLater P (â–· P) | 100.
 Proof. done. Qed.
 
 Global Instance frame_later R R' P Q Q' :
-  Frame R P Q → MakeLater Q Q' → IntoLater R' R → Frame R' (▷ P) Q'.
+  IntoLater R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLater=><- <- ->. by rewrite later_sep.
+  rewrite /Frame /MakeLater /IntoLater=>-> <- <-. by rewrite later_sep.
 Qed.
 
 Class MakeExceptLast (P Q : uPred M) := make_except_last : ◇ P ⊣⊢ Q.