proposition: Lemma SameValues_Fiat_Bind_TelEq : forall {av A B} (key: NameTag av B) compA compB tail ext, TelEq ext (Cons key (@Bind A B compA compB) tail) (Cons NTNone compA (fun a => Cons key (compB a) tail)).
proof: Proof. unfold TelEq; SameValues_Fiat_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes