proposition: Lemma Cons_PushExt: forall `{FacadeWrapper (Value av) A} (key : StringMap.key) (tail : A -> Telescope av) (ext : StringMap.t (Value av)) (v : A) (initial_state : StringMap.t (Value av)), initial_state ≲ Cons (NTSome key) (ret v) tail ∪ ext -> initial_state ≲ tail v ∪ [key |> wrap v]::ext.
proof: Proof. t__; apply SameValues_PushExt; try rewrite find_mapsto_iff; cleanup; eauto. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes