For brevity, we assume unless otherwise stated that arguments to tactics have the following types and uses:
An s suffix on the name of an argument indicates that it is a list. For example vs is considered to have type var list.
