From 3983fa93d66b81f5efe263dd7d084206215bfb3e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Wed, 28 Jul 2021 13:23:16 +0000
Subject: [PATCH] shorter proof

---
 theories/fin_maps.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8fce3468..687174b5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2064,8 +2064,7 @@ Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
 Lemma lookup_union_is_Some {A} (m1 m2 : M A) i :
   is_Some ((m1 ∪ m2) !! i) ↔ is_Some (m1 !! i) ∨ is_Some (m2 !! i).
 Proof.
-  unfold is_Some. setoid_rewrite lookup_union_Some_raw. split; [naive_solver|].
-  intros [[a Ha]|[a Ha]]; [naive_solver|].
+  rewrite <-!not_eq_None_Some, !lookup_union_None.
   destruct (m1 !! i); naive_solver.
 Qed.
 
-- 
GitLab