proposition: Lemma SameValues_MapsTo: forall `{FacadeWrapper (Value av) A} (key : String.string) (value : Comp A) (tail : A -> Telescope av) (ext state : StringMap.t (Value av)), state ≲ Cons (NTSome key) value tail ∪ ext -> exists v : A, value ↝ v /\ StringMap.MapsTo key (wrap v) state.
proof: Proof. simpl; intros. destruct (StringMap.find _ _) eqn: eq0; try tauto. rewrite <- find_mapsto_iff in *. repeat cleanup. eexists; intuition eauto. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid