- 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 *)