Re:Splitting and cut elimination

> *** Definition A deductive system is *Kai-esque* if every inference
> rule, apart from identity and cut, is such that all its instances in
> which an atom is substituted by a generic structure are derivable in
> the same system.

At first glance this reminds me of Belnap's condition C6/7:
 each rule is closed under simultaneous substitution of arbitrary
 structures for congruent parameters.

But perhaps your requirement that the new rule be derivable is
stronger?

Raj