diff --git a/algebra/cofe.v b/algebra/cofe.v
index a624a12fc13537e082a2142d2d4382d102d4d617..96ac25d19f45dac3d656b97f6c01be78e23234d5 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -323,9 +323,9 @@ Section product.
       apply (conv_compl n (chain_map snd c)).
   Qed.
   Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
-  Global Instance pair_timeless (x : A) (y : B) :
-    Timeless x → Timeless y → Timeless (x,y).
-  Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
+  Global Instance prod_timeless (x : A * B) :
+    Timeless (x.1) → Timeless (x.2) → Timeless x.
+  Proof. by intros ???[??]; split; apply (timeless _). Qed.
   Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC.
   Proof. intros ?? [??]; apply _. Qed.
 End product.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 9f50539601632fac061daa55e05fd2ea1c6449e1..84bc453741b239ec08271449b60e020d81204cc8 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -57,11 +57,6 @@ Proof. solve_proper. Qed.
 Global Instance slice_persistent γ P : PersistentP (slice N γ P).
 Proof. apply _. Qed.
 
-(* This should go automatic *)
-Instance box_own_auth_timeless γ
-  (a : auth (option (excl bool))) : TimelessP (box_own_auth γ a).
-Proof. apply own_timeless, pair_timeless; apply _. Qed.
-
 Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2.
 Proof.