proposition: Lemma SameValues_In_Ext_State: forall {av : Type} {tel: Telescope av} (key : StringMap.key) {ext st : StringMap.t (Value av)}, st ≲ tel ∪ ext -> StringMap.In key ext -> StringMap.In key st.
proof: Proof. intros ** h. apply In_MapsTo in h; destruct h. eapply MapsTo_In; eauto using SameValues_MapsTo_Ext_State. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid