pub fn then_all(t1: Tactic, t2: Tactic) -> Tactic
t1 <;> t2: run t1 on the focused goal, then t2 on every goal it produces.
t1 <;> t2
t1
t2