diff --git a/algebra/auth.v b/algebra/auth.v
index d21944475f33ad54505737effad941759247f6f4..c640860684da91ce9dad33dc9a54e6591d192546 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -50,8 +50,8 @@ Proof.
     apply (conv_compl (chain_map own c) n).
 Qed.
 Canonical Structure authC := CofeT auth_cofe_mixin.
-Instance Auth_timeless (ea : excl A) (b : A) :
-  Timeless ea → Timeless b → Timeless (Auth ea b).
+Global Instance auth_timeless (x : auth A) :
+  Timeless (authoritative x) → Timeless (own x) → Timeless x.
 Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
 Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
 Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
@@ -140,7 +140,7 @@ Proof.
   split; simpl.
   * by apply (@cmra_empty_valid A _).
   * by intros x; constructor; rewrite /= left_id.
-  * apply Auth_timeless; apply _.
+  * apply _.
 Qed.
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index a063d70d84e4867d5aeaa8728baad9dca171de1c..afffd9862562f774e5d7b73f27518fe3aebcc169 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -11,14 +11,6 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
-  (* Adding this locally only, since it overlaps with Auth_timelss in algebra/auth.v.
-     TODO: Would moving this to auth.v and making it global break things? *)
-  Local Instance AuthA_timeless (x : auth A) : Timeless x.
-  Proof.
-    (* FIXME: "destruct x; auto with typeclass_instances" should find this through Auth, right? *)
-    destruct x. apply Auth_timeless; apply _.
-  Qed.
-
   (* TODO: Need this to be proven somewhere. *)
   Hypothesis auth_valid :
     forall a b, (✓ Auth (Excl a) b : iPropG Λ Σ) ⊑ (∃ b', a ≡ b ⋅ b').