proposition: Lemma SameValues_forget_Ext: forall (av : Type) (tenv : Telescope av) (var : StringMap.key) (val2 : W) (ext : StringMap.t (Value av)) (st' : State av), var ∉ ext -> st' ≲ tenv ∪ [var |> wrap val2] :: ext -> st' ≲ tenv ∪ ext.
proof: Proof. induction tenv; SameValues_Facade_t. SameValues_Fiat_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas