proposition: Lemma SameValues_MapsTo_Ext_State_add: forall `{FacadeWrapper (Value av) A} {tel: Telescope av} (key : StringMap.key) {v: A} {ext st : StringMap.t (Value av)}, st ≲ tel ∪ [key |> wrap v]::ext -> StringMap.MapsTo key (wrap v) st.
proof: Proof. intros; eauto using SameValues_MapsTo_Ext_State, StringMap.add_1. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid