[Agda] type of []

[Sergei Meshveliani]

People,

In the proof

  take-n-[] :  {n : ℕ} → take n [] ≡ []
  take-n-[] {0}     =  refl
  take-n-[] {suc _} =  refl

Agda cannot derive the type of []. 
I can fix the signature in two ways.

  (I)
  take-n-[] :  ∀ {α} {A : Set α} {n}  → let []A : List A  -- lenghty   
                                            []A = []
                                        in 
                                        take n []A ≡ []

  (II)
  El : ∀ {a} (A : Set a) → A → A    -- for common usage
  El A x = x                        --
                                    --
  syntax El A x = x ∈: A            --

  take-n-[] :  ∀ {α} {A : Set α} {n} → take n ([] ∈: List A) ≡ []

What is a regular approach, please?

------
Sergei