Refiner.Sg
val formation : (Tactic.Tp.tac, Tactic.Tp.tac) quantifier
val intro : Tactic.Chk.tac -> Tactic.Chk.tac -> Tactic.Chk.tac
val pi1 : Tactic.Syn.tac -> Tactic.Syn.tac
val pi2 : Tactic.Syn.tac -> Tactic.Syn.tac