From a323b68e4f33fa4ab935b153456a0e7bb9beebee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 Mar 2020 20:08:48 +0100
Subject: [PATCH] Refactor proof of `elem_of_app`.

---
 theories/list.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 4d70d994..2a2a7946 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -791,9 +791,9 @@ Lemma not_elem_of_cons l x y : x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
 Proof. rewrite elem_of_cons. tauto. Qed.
 Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
 Proof.
-  induction l1.
-  - split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
-  - simpl. rewrite !elem_of_cons, IHl1. tauto.
+  induction l1 as [|y l1 IH]; simpl.
+  - rewrite elem_of_nil. naive_solver.
+  - rewrite !elem_of_cons, IH. naive_solver.
 Qed.
 Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
 Proof. rewrite elem_of_app. tauto. Qed.
-- 
GitLab