proposition: Lemma not_in_WeakEq_not_mapsto_adt: forall {av : Type} (name : StringMap.key) (ext : StringMap.t (Value av)) (initial_state : State av), name ∉ ext -> WeakEq ext initial_state -> not_mapsto_adt name initial_state = true.
proof: Proof. unfold WeakEq; intros; intuition (eauto using not_in_SameADTs_not_mapsto_adt). Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas