partial def Lean.Meta.Sym.Simp.simpTelescope : Simproc

Simplify telescope binders (have-expression values, and arrow hypotheses) but not the final body. This simproc is useful to simplify target before introducing.