fact: Definition Lifted_not_mapsto_adt {av} ext tenv k := @LiftPropertyToTelescope av ext (fun map => not_mapsto_adt k map = true) tenv.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid