+ apply ALeft.
+ apply ACanL.
+
+ destruct case_RCut.
+ simpl.
+ destruct l as [|ec lev]; simpl.
+ apply nd_rule.
+ replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
+ apply RCut.
+ induction Σ₁₂; try destruct a; auto.
+ simpl.
+ rewrite <- IHΣ₁₂1.
+ rewrite <- IHΣ₁₂2.
+ reflexivity.
+ simpl.
+ repeat drop_simplify.
+ simpl.
+ repeat take_simplify.
+ simpl.
+ set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
+ rewrite take_lemma'.
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+ apply nd_prod.
+ apply nd_id.
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply ARight.
+ unfold x1.
+ rewrite drop_to_nothing.
+ apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
+ admit. (* OK *)
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
+ set (mapOptionTree flatten_type Σ₁₂) as a.
+ set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
+ set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ simpl.
+ eapply ga_first.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+ simpl.
+ apply precompose.
+
+ destruct case_RLeft.
+ simpl.
+ destruct l as [|ec lev].
+ simpl.
+ replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
+ apply nd_rule.
+ apply RLeft.
+ induction Σ; try destruct a; auto.
+ simpl.
+ rewrite <- IHΣ1.
+ rewrite <- IHΣ2.
+ reflexivity.
+ repeat drop_simplify.
+ rewrite drop_to_nothing.
+ simpl.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply ARight.
+ apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
+ admit (* FIXME *).
+ idtac.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
+ apply boost.
+ take_simplify.
+ simpl.
+ replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ apply ga_second.
+ rewrite take_lemma'.
+ reflexivity.
+
+ destruct case_RRight.
+ simpl.
+ destruct l as [|ec lev].
+ simpl.
+ replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
+ apply nd_rule.
+ apply RRight.
+ induction Σ; try destruct a; auto.
+ simpl.
+ rewrite <- IHΣ1.
+ rewrite <- IHΣ2.
+ reflexivity.
+ repeat drop_simplify.
+ rewrite drop_to_nothing.
+ simpl.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply ALeft.
+ apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
+ admit (* FIXME *).
+ idtac.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
+ apply boost.
+ take_simplify.
+ simpl.
+ replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ apply ga_first.
+ rewrite take_lemma'.
+ reflexivity.