proposition: Lemma not_In_Telescope_not_in_Ext_not_mapsto_adt : forall {av} tenv k st ext, k ∉ ext -> @NotInTelescope av k tenv -> st ≲ tenv ∪ ext -> not_mapsto_adt k st = true.
proof: Proof. induction tenv; SameValues_Facade_t. destruct key; SameValues_Facade_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas