proposition: Lemma Lifted_not_In_Telescope_not_in_Ext_not_mapsto_adt: forall `{FacadeWrapper (Value av) A} ext k tenv, k ∉ ext -> NotInTelescope k tenv -> @Lifted_not_mapsto_adt av ext tenv k.
proof: Proof. unfold Lifted_not_mapsto_adt, LiftPropertyToTelescope; intros. eauto using not_In_Telescope_not_in_Ext_not_mapsto_adt. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas