[Agda] rewriting product types vs. single ctor data/record types

[Jonathan Leivent]

I had thought that a type like

Σ[ a ∈ A ] Σ[ b ∈ B ] Σ[c ∈ C ] (D a b c)

wouldn't be any easier to use - and actually less "nice" than its 
fully-named counterpart:

record DR : Set _ where
   field
     a : A
     b : B
     c : C
     d : D a b c

or a similar single ctor inductive data type.  However, the (dependent) 
product type seems more rewritable:  if you have just "DR" as a goal, 
you can't use rewrite to help you fit things into its fields; but if you 
have that messy (dependent) product, the types of the fields (A, B, C) 
are part of the type itself - hence visible in the goal - and so can be 
targeted by rewriting.

Is there a way around this?  Is there some way to rewrite "into" the 
fields of a data/record type that appears as a goal, to achieve the same 
effect as rewriting would on a very similar product type?

-- Jonathan