%%% Termination of cut-elimination

%terminates {A [D E]}
(ca' A D E _).

%terminates D (ce' D _).