Final sugared generic eliminator for Desc/Mu in Agda model.

This combines the case eliminator for tags with the
projecting + substituting eliminator for Mu.

The result is specialized to tagged descriptions, which result from
elaborating datatype declarations.