proposition: Lemma SameValues_Add_Cons: forall `{FacadeWrapper (Value av) A} (key : StringMap.key) (value: A) (ext state : StringMap.t (Value av)), key ∉ ext -> WeakEq ext state -> [key |> (wrap value)]::state ≲ ([[ `key ->> value as _ ]] :: Nil) ∪ ext.
proof: Proof. intros; apply Cons_PopExt; simpl; eauto using WeakEq_Refl, WeakEq_add. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes