Module Refiner.Prf

val formation : Tactic.Chk.tac -> Tactic.Tp.tac
val intro : Tactic.Chk.tac