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