+ eapply AComp.
+ eapply AuAssoc.
+ apply ALeft.
+ eapply AuAssoc.
+
+ destruct case_RCut.
+ simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
+ set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
+ set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
+ destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+ destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+ rewrite <- e.
+ eapply nd_comp.
+ eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
+ apply nd_prod.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply ALeft.
+ destruct s.
+ eapply arrangeCancelEmptyTree with (q:=x).
+ rewrite e0.
+ admit. (* FIXME, but not serious *)
+ apply nd_id.
+
+ destruct case_RLeft.
+ simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+ set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+ set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+ destruct (decide_tree_empty (Σ' @@@ (h::l)));
+ [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+ destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+ rewrite <- e.
+ clear Σ'' e.
+ destruct s.
+ set (arrangeUnCancelEmptyTree _ _ e) as q.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+ apply nd_rule.
+ eapply SFlat.
+ eapply RLeft.
+
+ destruct case_RRight.
+ simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+ set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+ set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+ destruct (decide_tree_empty (Σ' @@@ (h::l)));
+ [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+ destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+ rewrite <- e.
+ clear Σ'' e.
+ destruct s.
+ set (arrangeUnCancelEmptyTree _ _ e) as q.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ]. (* yuck *)
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+ eapply nd_rule.
+ eapply SFlat.
+ apply RRight.