YES
ignored inputs:
(COMMENT an orthogonal explicit substitution calculus for lambda terms )
(COMMENT Example 8 of [ SKAT15 , doi:10.4230/LIPIcs.RTA.2015.301 ] )

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