-Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
-| RCanL : ∀ t a , URule [Γ>>Δ> [],,a |- t ] [Γ>>Δ> a |- t ]
-| RCanR : ∀ t a , URule [Γ>>Δ> a,,[] |- t ] [Γ>>Δ> a |- t ]
-| RuCanL : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> [],,a |- t ]
-| RuCanR : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> a,,[] |- t ]
-| RAssoc : ∀ t a b c , URule [Γ>>Δ>a,,(b,,c) |- t ] [Γ>>Δ>(a,,b),,c |- t ]
-| RCossa : ∀ t a b c , URule [Γ>>Δ>(a,,b),,c |- t ] [Γ>>Δ> a,,(b,,c) |- t ]
-| RLeft : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c)
-| RRight : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
-| RExch : ∀ t a b , URule [Γ>>Δ> (b,,a) |- t ] [Γ>>Δ> (a,,b) |- t ]
-| RWeak : ∀ t a , URule [Γ>>Δ> [] |- t ] [Γ>>Δ> a |- t ]
-| RCont : ∀ t a , URule [Γ>>Δ> (a,,a) |- t ] [Γ>>Δ> a |- t ].
-
+Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
+| 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
+.