Refiner.Dim
val formation : Tactic.Tp.tac
val dim0 : Tactic.Chk.tac
val dim1 : Tactic.Chk.tac
val literal : int -> Tactic.Chk.tac