proposition: Lemma WeakEq_Mapsto_MapsTo: forall {av : Type} {key : StringMap.key} {ext st : StringMap.t (Value av)} {v : Value av}, StringMap.MapsTo key v ext -> WeakEq ext st -> StringMap.MapsTo key v st.
proof: Proof. unfold WeakEq, SameSCAs, SameADTs. intros ** v ? ?. destruct v; firstorder. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid