in calculation, allongside \ref and \eqref, it is now possible to refer to theorems (or axioms or invariants, etc) with inst and eqinst. They are convenient in the case where the theorem is a universal quantification and the user wants to handpick an instantiation. It can be done with the following syntax:

\eqinst{thm3}{ \subst{x}{ x \uparrow y } and \subst{y}{k} }.

All the variables do not need to be instantiate at once by this scheme.