Telescope (cooltt.Core.Refiner.Telescope)

val empty : Tactic.Tele.tac

val cell : (Tactic.Tp.tac, Tactic.Tele.tac) quantifier

val include_ : 
  (Ident.t -> Ident.t option) ->
  Tactic.Tele.tac ->
  (Tactic.Var.tac list -> Tactic.Tele.tac) ->
  Tactic.Tele.tac

val el : Tactic.KanTele.tac -> Tactic.Tele.tac