signature stack_introLib =
sig

  val STACK_INTRO_RULE : int list -> Thm.thm -> Thm.thm

end