YES
ignored inputs:
(COMMENT structural substitution for lambda-mu-terms [ Parigot05 , doi:10.1007/BFb0013061 ] )

NRS:
   [ (0):  |- (ssub <[a]b,c,[]X>) -> b,
     (1): b#X |- (ssub <[a](lam [b][]Y),c,[]X>) -> (lam [b](ssub <[a][]Y,c,[]X>)),
     (2):  |- (ssub <[a](app <[]Y,[]Z>),b,[]X>) -> (app <(ssub <[a][]Y,b,[]X>),(ssub <[a][]Z,b,[]X>)>),
     (3): b#X |- (ssub <[a](mu [b][]Y),c,[]X>) -> (mu [b](ssub <[a][]Y,c,[]X>)),
     (4):  |- (ssub <[a](ind <a,[]Y>),b,[]X>) -> (ind <b,(app <(ssub <[a][]Y,b,[]X>),[]X>)>),
     (5):  |- (ssub <[a](ind <b,[]Y>),c,[]X>) -> (ind <b,(ssub <[a][]Y,c,[]X>)>) ]
Check confluence by orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
no proper overlaps
result: YES
time: 8 msec.