proposition: Lemma SameValues_Push_ret: forall `{H : FacadeWrapper (Value av) A} (k : string) (tenv : A -> Telescope av) (ext : StringMap.t (Value av)) (initial_state : State av) (a : A), StringMap.MapsTo k (wrap a) initial_state -> StringMap.remove k initial_state ≲ tenv a ∪ ext -> initial_state ≲ [[`k ->> a as vv0]]::tenv vv0 ∪ ext.
proof: Proof. SameValues_Fiat_t. SameValues_Facade_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas