- [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ].
- 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 ].
+ [ Γ > Δ > [a @@ lev],,Σ |- [ s @@ lev ] ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].