Refiner.Circle
val formation : Tactic.Tp.tac
val base : Tactic.Chk.tac
val loop : Tactic.Chk.tac -> Tactic.Chk.tac
val elim : Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Syn.tac -> Tactic.Syn.tac