diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 910e124da15762ad41df3e314f6532d82acf87bb..6f19ff730fa215f7a0bbd8283b41b44ab2e7b022 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -57,6 +57,11 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 
+Global Instance map_timeless `{!∀ a : A, Timeless a} (g : gmap K A) : Timeless g.
+Proof.
+  intros m Hm i. apply timeless; eauto with typeclass_instances.
+Qed.
+
 Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
diff --git a/algebra/option.v b/algebra/option.v
index dafa849abd013a21ce5268e6d70b004f8a6f5ca7..94eeac7aabf81d9a3a15e8cf21bbfbd9841b48fc 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -51,6 +51,8 @@ Global Instance None_timeless : Timeless (@None A).
 Proof. inversion_clear 1; constructor. Qed.
 Global Instance Some_timeless x : Timeless x → Timeless (Some x).
 Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
+Global Instance option_timeless `{!∀ a : A, Timeless a} (mx : option A) : Timeless mx.
+Proof. destruct mx; auto with typeclass_instances. Qed.
 End cofe.
 
 Arguments optionC : clear implicits.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 65bd7e42c1a9dd3a5c8f7ce262bf90f8ed609e44..608410086b108e74d91f207895684aebef9f924c 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -62,7 +62,7 @@ Section auth.
     apply (eq_rewrite b (a â‹… a')
               (λ x, ■✓x ★ ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
     { by move=>n ? ? /timeless_iff ->. }
-    { apply sep_elim_l', sep_elim_r'. done. (* FIXME why does "eauto using I" not work? *) }
+    { by eauto with I. }
     rewrite const_equiv // left_id comm.
     apply sep_mono; first done.
     by rewrite sep_elim_l.
@@ -84,7 +84,7 @@ Section auth.
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
   Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
-        `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
+        L `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
     P ⊑ (auth_own AuthI γ a ★ (∀ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') -★