Refiner.Cof
val formation : Tactic.Tp.tac
val eq : Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Chk.tac
val le : Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Chk.tac
val join : Tactic.Chk.tac list -> Tactic.Chk.tac
val meet : Tactic.Chk.tac list -> Tactic.Chk.tac
val boundary : Tactic.Chk.tac -> Tactic.Chk.tac
val split : branch_tac list -> Tactic.Chk.tac