proposition: Lemma SameValues_Cons_unfold_Some : forall `{FacadeWrapper (Value av) A} k (st: State av) val ext tail, st ≲ (Cons (NTSome k) val tail) ∪ ext -> exists v: A, StringMap.MapsTo k (wrap v) st /\ val ↝ v /\ StringMap.remove k st ≲ tail v ∪ ext.
proof: Proof. simpl; intros; repeat match goal with | _ => exfalso; assumption | [ H: match ?x with Some _ => _ | None => False end |- _ ] => let _eq := fresh in destruct x eqn:_eq | _ => cleanup | _ => intuition eauto using StringMap.find_2 end. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas