diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 98b903d8980b2f6fdd4b7b96d8ddbedfa188d404..c6c897cbe4b616d6563585a1e3ea14a608812780 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -937,11 +937,8 @@ Qed.
 Global Instance forall_timeless {A} (Ψ : A → uPred M) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
 Proof.
-  rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
-  apply or_mono; first done. apply forall_intro=> x.
-  rewrite -(löb (Ψ x)); apply impl_intro_l.
-  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite impl_elim_r (forall_elim x).
+  rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
+  apply forall_mono; auto.
 Qed.
 Global Instance exist_timeless {A} (Ψ : A → uPred M) :
   (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).