- { se_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
- ; se_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
+ { se_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma]
+ ; se_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau]
+
+ (* left and right expansion must commute with cut *)
+ ; se_reflexive_left : ∀ a c, nd_seq_reflexive a;; [#se_expand_left c#] === nd_seq_reflexive (c,, a)
+ ; se_reflexive_right : ∀ a c, nd_seq_reflexive a;; [#se_expand_right c#] === nd_seq_reflexive (a,, c)
+ ; se_cut_left : ∀ a b c d, [#se_expand_left _#]**[#se_expand_left _#];;nd_cut _ _ _===nd_cut a b d;;[#se_expand_left c#]
+ ; se_cut_right : ∀ a b c d, [#se_expand_right _#]**[#se_expand_right _#];;nd_cut _ _ _===nd_cut a b d;;[#se_expand_right c#]