- eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
- eapply nd_comp; [ apply nd_rlecnac | idtac ].
- apply nd_prod.
- apply nd_id.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.