KanTelescope (cooltt.Core.Refiner.KanTelescope)

val empty : Tactic.KanTele.tac

val cell : (Tactic.Chk.tac, Tactic.KanTele.tac) quantifier

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