fact: Fixpoint tele_app {TT : tele} {U} : (TT -t> U) -> TT → U := match TT as TT return (TT -t> U) -> TT → U with | TeleO => λ F _, F | TeleS r => λ (F : TeleS r -t> U) '(TeleArgCons x b), tele_app (F x) b end.
imports: stdpp(base tactics) stdpp(options)