-(* Figure 3, production $\vdash_E$, Uniform rules *)
-Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
-| RId : forall a , Arrange a a
-| RCanL : forall a , Arrange ( [],,a ) ( a )
-| RCanR : forall a , Arrange ( a,,[] ) ( a )
-| RuCanL : forall a , Arrange ( a ) ( [],,a )
-| RuCanR : forall a , Arrange ( a ) ( a,,[] )
-| RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
-| RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
-| RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
-| RWeak : forall a , Arrange ( [] ) ( a )
-| RCont : forall a , Arrange ( (a,,a) ) ( a )
-| RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
-| RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
-| RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
-.
-