diff --git a/algebra/auth.v b/algebra/auth.v
index 26dbe5652013247c4d09da31de72f8afa8188348..7d04ae801c93cb5a38f1e18e61e1980a117cb7ae 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -156,7 +156,6 @@ Proof.
   split; simpl.
   - apply (@ucmra_unit_valid A).
   - by intros x; constructor; rewrite /= left_id.
-  - apply _.
   - do 2 constructor; simpl; apply (persistent_core _).
 Qed.
 Canonical Structure authUR :=
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 642a4dc62031e1be4505a34be0248f32808baa79..8d6f666a8b1962b3dac3234f62cbf59635b67097 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -153,7 +153,6 @@ Arguments core' _ _ _ /.
 Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
   mixin_ucmra_unit_valid : ✓ ∅;
   mixin_ucmra_unit_left_id : LeftId (≡) ∅ (⋅);
-  mixin_ucmra_unit_timeless : Timeless ∅;
   mixin_ucmra_pcore_unit : pcore ∅ ≡ Some ∅
 }.
 
@@ -201,8 +200,6 @@ Section ucmra_mixin.
   Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
   Global Instance ucmra_unit_left_id : LeftId (≡) ∅ (@op A _).
   Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
-  Global Instance ucmra_unit_timeless : Timeless (∅ : A).
-  Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
   Lemma ucmra_pcore_unit : pcore (∅:A) ≡ Some ∅.
   Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
 End ucmra_mixin.
@@ -922,7 +919,6 @@ Section prod_unit.
     split.
     - split; apply ucmra_unit_valid.
     - by split; rewrite /=left_id.
-    - by intros ? [??]; split; apply (timeless _).
     - rewrite prod_pcore_Some'; split; apply (persistent _).
   Qed.
   Canonical Structure prodUR :=
@@ -1063,7 +1059,7 @@ Section option.
 
   Instance option_empty : Empty (option A) := None.
   Lemma option_ucmra_mixin : UCMRAMixin optionR.
-  Proof. split. done. by intros []. by inversion_clear 1. done. Qed.
+  Proof. split. done. by intros []. done. Qed.
   Canonical Structure optionUR :=
     UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
 
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 55a18a326804262376bc3cce30f1821b69813250..8d2fe2b1ab6db192688e3fbfc48db8fcb90c75b3 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -62,7 +62,7 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 
-Instance gmap_empty_timeless : Timeless (∅ : gmap K A).
+Global Instance gmap_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
   inversion_clear Hm; constructor.
@@ -173,7 +173,6 @@ Proof.
   split.
   - by intros i; rewrite lookup_empty.
   - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
-  - apply gmap_empty_timeless.
   - constructor=> i. by rewrite lookup_omap lookup_empty.
 Qed.
 Canonical Structure gmapUR :=
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 782b9df96ffb25bc75cd19ea8d19fdf305603fcc..181e5d80de9b0a417e2818a7ae79cb87e67c8289 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -135,12 +135,15 @@ Section iprod_cmra.
     split.
     - intros x; apply ucmra_unit_valid.
     - by intros f x; rewrite iprod_lookup_op left_id.
-    - intros f Hf x. by apply: timeless.
     - constructor=> x. apply persistent_core, _.
   Qed.
   Canonical Structure iprodUR :=
     UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
 
+  Global Instance iprod_empty_timeless :
+    (∀ i, Timeless (∅ : B i)) → Timeless (∅ : iprod B).
+  Proof. intros ? f Hf x. by apply: timeless. Qed.
+
   (** Internalized properties *)
   Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
   Proof. by uPred.unseal. Qed.
@@ -196,7 +199,8 @@ Section iprod_singleton.
   Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
 
   Global Instance iprod_singleton_timeless x (y : B x) :
-    Timeless y → Timeless (iprod_singleton x y) := _.
+    (∀ i, Timeless (∅ : B i)) →  Timeless y → Timeless (iprod_singleton x y).
+  Proof. apply _. Qed.
 
   Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
   Proof.
diff --git a/algebra/list.v b/algebra/list.v
index 38fc3a495a7906bdc80b922e668c992782773ea1..373ea50573750d3f3ef3af6bf95436a26b60d9b1 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -210,7 +210,6 @@ Section cmra.
     split.
     - constructor.
     - by intros l.
-    - by inversion_clear 1.
     - by constructor.
   Qed.
   Canonical Structure listUR :=