Separate file for new tactics
Generic theorems about sets (represented as lists) in a new file
Separate tactics