Dear all, I modified the decomposition theorem so that DPs in no component are dealt with automatically. So, now, <decomp> with <unif> should work. You should use it instead of <scc_decomp> (and <hde>). But, since I have no prover, I cannot check it on many examples.