- | 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
+ | AId : forall a , Arrange a a
+ | ACanL : forall a , Arrange ( [],,a ) ( a )
+ | ACanR : forall a , Arrange ( a,,[] ) ( a )
+ | AuCanL : forall a , Arrange ( a ) ( [],,a )
+ | AuCanR : forall a , Arrange ( a ) ( a,,[] )
+ | AAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
+ | AuAssoc : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
+ | AExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
+ | AWeak : forall a , Arrange ( [] ) ( a )
+ | ACont : forall a , Arrange ( (a,,a) ) ( a )
+ | ALeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
+ | ARight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
+ | AComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c