having now proved invertibility of multiples of logical rules gen_inv_wc,
to use this in proving admissibility of cut (NOT multicut) we need to use
invertibility for cut on non-atomic logical formulae,
but for atoms we need to look at a derivation tree which explicitly does not
have a weakening (on the cut-formula) above the last lot of contractions, and
some similar requirements.
Also we need to extend the invertibility lemmas to where there are additional
rules eg introducing box X |- box B