Add lookupb_remove_not_in

2 files changed, 8 insertions, 1 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}
diff --git a/src/Compilers/Named/ContextProperties/Tactics.v b/src/Compilers/Named/ContextProperties/Tactics.v
index 9616725d6..f438d5444 100644
--- a/src/Compilers/Named/ContextProperties/Tactics.v
+++ b/src/Compilers/Named/ContextProperties/Tactics.v
@@ -37,7 +37,8 @@ Ltac inversion_step :=
 Ltac rewrite_lookupb_extendb_step :=
   first [ rewrite lookupb_extendb_different by congruence
         | rewrite lookupb_extendb_same
-        | rewrite lookupb_extendb_wrong_type by assumption ].
+        | rewrite lookupb_extendb_wrong_type by assumption
+        | rewrite lookupb_removeb by congruence ].
 Ltac specializer_t_step :=
   match goal with
   | _ => progress specialize_by_assumption