proposition: Lemma DropName_remove : forall {av} (tenv: Telescope av) k ext st, k ∉ ext -> st ≲ tenv ∪ ext -> StringMap.remove k st ≲ (DropName k tenv) ∪ ext.
proof: Proof. induction tenv; repeat match goal with | _ => SameValues_Facade_t_step | [ key: NameTag _ _ |- _ ] => destruct key | [ |- context[string_dec ?x ?y] ] => destruct (string_dec x y) | _ => progress simpl | [ |- exists _, _ ] => eexists end; try solve [simpl; eauto using M.remove_2 with SameValues_db]; [ rewrite <- remove_remove_redundant | rewrite remove_remove_comm ]; eauto using M.remove_2. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas