fact: Fixpoint tele_map {T U} {TT : tele} : (T → U) → (TT -t> T) → TT -t> U := match TT as TT return (T → U) → (TT -t> T) → TT -t> U with | TeleO => λ F : T → U, F | @TeleS X b => λ (F : T → U) (f : TeleS b -t> T) (x : X), tele_map F (f x) end.
imports: stdpp(base tactics) stdpp(options)