[Agda] tuple selectors

[Sergei Meshveliani]

People,
This may concern lib-0.7.
I do not find a natural access to a tuple field.

1) Pattern matching does not work in the construct of
   ...
      where
      (_ , _ , z, _) = p

(it needs a more complicated code).

2) I wonder of whether I need to use  records  everywhere for tuples.

3) Setting to the code the compositions like  proj₁ ∘ proj₂ ∘ proj₂ 
   is much less writable and readable than  `tuple43'.

So, I define the selectors like

  tuple43 : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} 
                                                {D : Set d} → 
                                                       A × B × C × D → C
  tuple43 = proj₁ ∘ proj₂ ∘ proj₂ 

Am I missing something?
Does Standard library need to include several  tuple-ij  selectors?

Regards,

------
Sergei