Refiner.Sub
val formation : Tactic.Tp.tac -> Tactic.Chk.tac -> (Tactic.var -> Tactic.Chk.tac) -> Tactic.Tp.tac
val intro : Tactic.Chk.tac -> Tactic.Chk.tac
val elim : Tactic.Syn.tac -> Tactic.Syn.tac