proposition: Lemma Lifted_MapsTo_SCA_not_mapsto_adt: forall {av} ext k (v: W) tenv, StringMap.MapsTo k (SCA _ v) ext -> @Lifted_not_mapsto_adt av ext tenv k.
proof: Proof. unfold Lifted_not_mapsto_adt, LiftPropertyToTelescope; intros. SameValues_Facade_t. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas