From 76dec75fd02faacf6a140fb54b03174587874ee6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Feb 2018 21:20:57 +0100
Subject: [PATCH] Remove temp lemma.

---
 theories/proofmode/coq_tactics.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 50073499e..b75575865 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -694,10 +694,6 @@ Proof.
 Qed.
 
 (** * Implication and wand *)
-Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
-  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ∗ □?p Q ⊢ of_envs Δ'.
-Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
-
 Lemma tac_impl_intro Δ Δ' i P P' Q R :
   FromImpl R P Q →
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
-- 
GitLab