fact: Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y) : (TT -t> X) → Y := (fix rec {TT} : (TT -t> X) → Y := match TT as TT return (TT -t> X) → Y with | TeleO => λ x : X, base x | TeleS b => λ f, step (λ x, rec (f x)) end) TT.
imports: stdpp(base tactics) stdpp(options)