From 170c76a39b28f5d3b73b73c610a741ea8f44bd54 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Nov 2017 17:50:39 +0100
Subject: [PATCH] Simplify proof of `forall_timeless`.

---
 theories/base_logic/derived.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 98b903d89..c6c897cbe 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).
-- 
GitLab