proposition: Lemma TelAppend_Nil {av} : forall t: Telescope av, TelStrongEq (TelAppend t Nil) t.
proof: Proof. induction t; simpl. + reflexivity. + econstructor; eauto with typeclass_instances. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedPropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas