proposition: Lemma SameValues_MapsTo_ret_ex: forall `{H: 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, value ↝ v /\ state ≲ Cons (NTSome key) (ret v) tail ∪ ext.
proof: Proof. t__. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid