proposition: Lemma Cons_PopExt: 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)), key ∉ ext -> initial_state ≲ tail v ∪ [key |> wrap v]::ext -> initial_state ≲ Cons (NTSome key) (ret v) tail ∪ ext.
proof: Proof. t__. repeat match goal with | [ H: ?st ≲ ?tel ∪ [?k |> wrap ?v]::ext |- _ ] => let h := fresh in pose proof H as h; apply SameValues_MapsTo_Ext_State_add in h; no_duplicates | [ H: StringMap.MapsTo ?k ?v ?m |- match StringMap.find ?k ?m with _ => _ end] => rewrite find_mapsto_iff in H; rewrite H | _ => cleanup end; eauto using SameValues_PopExt. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes