proposition: Lemma SameValues_add_W_notIn_ext : forall {av} k (v: W) (st: StringMap.t (Value av)) tenv ext, k ∉ ext -> NotInTelescope k tenv -> st ≲ tenv ∪ ext -> StringMap.add k (wrap v) st ≲ tenv ∪ ext.
proof: Proof. eauto with SameValues_db. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas