Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption
split_and, the new tactics are
split_or? H and
split_or! H. The name
H is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).
I was pondering whether the tactic should be
split_or H or
split_or in H. The second one follows the usual pattern of
in+assumption, but at the same time there is not going to be a
split_or tactic that works on the goal, so...