[Agda] not-all -> any-not

[Sergei Meshveliani]

People,
I write

  ¬all→any¬ : {A : Set} {P : A → Set} {P? : Decidable P} {xs : List A} →
                                      (¬ All P xs) → (Any (¬_ ∘ P) xs)

and think:  is this provable without using  Decidable ?

I tried a singleton list for a counter example. But here is the proof: 

 ¬all→P1 : {A : Set} {P : A → Set} {x : A} → (¬ All P (x ∷ [])) → ¬ P x
 ¬all→P1 ¬all-x Px =  ¬all-x (Px ∷a []a)

([]a, _∷a_  imported from  Data.List.All  as renamed [], _∷_).

May be   x ∷ y ∷ []   is a counter example?


And  ¬all→any¬  I implement as

  ¬all→any¬              {xs = []}     ¬all[]     =  ⊥-elim $ ¬all[] []a

  ¬all→any¬ {P = P} {P? = P?} {xs = x ∷ ys} ¬all-x:ys  with P? x
  ...      |
             no ¬Px = here ¬Px
  ...      | yes Px = 
                 there $ ¬all→any¬ {P = P} {P? = P?} {xs = ys} ¬all-ys
                              where
                              ¬all-ys : ¬ All P ys
                              ¬all-ys all-ys = ¬all-x:ys (Px ∷a all-ys)


Thank you in advance for explanation,

------
Sergei