(* 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 )
Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
intros.
induction X; simpl.
+ apply RId.
apply RCanL.
apply RCanR.
apply RuCanL.