fact: Fixpoint Telescope_append (t : Telescope) : flattenT t Type -> Telescope := match t return flattenT t _ -> _ with | bottom => fun X => @tele X (fun _ => bottom) | tele A B => fun X => @tele A (fun a => Telescope_append (B a) (X a)) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Relations.Relation_Definitions Coq.Classes.Morphisms