%worlds (conbind-reg | termbind-reg | modbind-reg) 
(expr-elab-reg _ _ _) 
(expr-row-elab-reg _ _ _ _) 
(match-elab-reg _ _ _ _ _)
(match-spine-elab-reg _ _ _ _ _ _)
(pat-elab-reg _ _ _ _ _)
(pat-row-elab-reg _ _ _ _ _)
(dec-elab-reg _ _ _)
(funbind-elab-reg _ _ _ _ _)
(functorbind-elab-reg _ _ _)
(strexp-elab-reg _ _ _)
(spec-elab-reg _ _ _)
(sigexp-elab-reg _ _ _)
(functorspec-elab-reg _ _ _).

%total (D1 D2 D3 D4 D5 D6 D7 D8 D9 D10 D11 D12 D13)
(expr-elab-reg _ D1 _) 
(expr-row-elab-reg _ _ D2 _) 
(match-elab-reg _ _ _ D3 _)
(match-spine-elab-reg _ _ _ _ D4 _)
(pat-elab-reg _ _ _ D5 _)
(pat-row-elab-reg _ _ _ D6 _)
(dec-elab-reg _ D7 _)
(funbind-elab-reg _ _ _ D8 _)
(functorbind-elab-reg _ D9 _)
(strexp-elab-reg _ D10 _)
(spec-elab-reg _ D11 _)
(sigexp-elab-reg _ D12 _)
(functorspec-elab-reg _ D13 _).