Refiner.Pi
val formation : (Tactic.Tp.tac, Tactic.Tp.tac) quantifier
val intro : ?ident:Ident.t -> (Tactic.var -> Tactic.Chk.tac) -> Tactic.Chk.tac
val apply : Tactic.Syn.tac -> Tactic.Chk.tac -> Tactic.Syn.tac