[Agda] about Null

[Sergei Meshveliani]

People,

I introduce 

  data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []

for expressing the predicate  "a list is empty". 
Then, I need to prove the following two simple statements
(¬Null→length>0, a ≢ 0). And fail.
Can you, please demonstrate a proof?

------------------------------------------------------------------------
open import Level using (Level)
open import Function using (case_of_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Empty       using (⊥; ⊥-elim)
open import Data.Nat         using (ℕ; suc; _>_; _≤_; s≤s; z≤n)
open import Data.List        using (List; []; _∷_; length)
open import Data.Product     using (_,_)

data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []

null? : {α : Level} → {A : Set α} → (xs : List A) → Dec (Null xs)
null? []      = yes isNull
null? (_ ∷ _) = no λ()

suc>0 : ∀ {n} → suc n > 0
suc>0 = s≤s z≤n

¬Null→length>0 : {α : Level} → {A : Set α} → (xs : List A) → ¬ Null xs →
                                                           length xs > 0
¬Null→length>0 (_ ∷ _) _  =  suc>0
¬Null→length>0 [] ()                 -- fails


-- Prove  a ≢ 0  from these postulated things:

postulate anything      : ∀ {a} {A : Set a} → A
          items         : ℕ → List ℕ
          a             : ℕ
          nullItems→a≢0 : Null (items a) → a ≢ 0
          lnItems>0→a≢0 : length (items a) > 0 → a ≢ 0

a≢0 : a ≢ 0
a≢0 = go (items a) PE.refl (null? (items a))
    where
    go : (its : List ℕ) → its ≡ (items a) → Dec (Null (items a)) → a ≢ 0
    go _ _ (yes nullIts-a)   =  nullItems→a≢0 nullIts-a
    -- go _ _ (no notNullIts-a =  
    -- ?
-------------------------------------------------------------------------