1 files changed, 6 insertions, 0 deletions
diff --git a/src/Compilers/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v
index 1db840753..9956f3b48 100644
--- a/src/Compilers/Named/ContextProperties.v
+++ b/src/Compilers/Named/ContextProperties.v
@@ -52,6 +52,12 @@ Section with_context.
       = find_Name_and_val t n N v (lookupb ctx n t).
   Proof using ContextOk. revert ctx; induction T; t. Qed.
 
+  Lemma lookupb_remove_not_in (ctx : Context)
+        T N t n
+        (H : @find_Name n T N = None)
+    : lookupb (remove ctx N) n t = lookupb ctx n t.
+  Proof using ContextOk. revert ctx; induction T; t. Qed.
+
   Lemma find_Name_and_val_Some_None
         {var' var''}
         {t n T N}