o in proofs, the subproof of assertions can refer to one another in an acyclic manner
o a new command, \using, is available in proofs. It takes one argument that can be any one of \ref, \eqref, \inst, \eqinst. It adds the reference theorems to the set of assumptions. It is especially useful with the tactics easy, indirect (in)equality and symmetry in order to feed a theorem to Z3