rotate_tac

Rotates the assumptions by k positions to the left.

It can be used to influence which assumption is unified when using methods like drule, frule, erule or even Assumption.