proposition: Lemma SameValues_Nil_inv : forall (A : Type) (state ext : StringMap.t (Value A)), WeakEq ext state -> state ≲ Nil ∪ ext.
proof: Proof. intros; assumption. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas