[Agda] matching against _::_ ?

[Sergei Meshveliani]

People,

I have a function of kind

  let a = gen 1
      b = gen 2
      c = gen 3
      d = gen 4
      e = gen 5
      f = gen 6
      g = gen 7
  in
  F a b (c d) (H e f g)

And in other examples there may be more `gen' values of this kind. 

Is it possible a shorter expression?

For the construct of kind 

  let  a ∷ b ∷ c ∷ _ =  gen 1 ∷ gen 2 ∷ gen 3 ∷ []
  in   ...

Agda reports  "Expected record pattern ...".
Why?

And with
   case gen 1 ∷ gen 2 ∷ gen 3 ∷ []
   of
   { (a ∷ b ∷ c ∷ _) → a + b + c 
   ; _               → ?? 
   },

I do not see how to eliminate the remaining patterns in a short code.

How to make Agda accept that the list  gen 1 ∷ gen 2 ∷ gen 3 ∷ [] 
has at least three members, and to pattern-match accordingly?

What may be a way out?

Thanks,

------
Sergei