[Agda] suc suc _ : Bit

[Sergei Meshveliani]

Please, how to fix the below  positive-add1  (last clause) ?

--------------------------------------------------------------------
open import Level using () renaming (zero to 0ℓ)
open import Relation.Nullary.Core using (¬_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List  using ([]; _∷_)
open import Data.Fin   using (Fin) renaming (zero to 0b; suc to sucB)
open import Data.Digit using (Bit)
open import Data.Bin   using (Bin⁺; addCarryToBitList)

1b : Bit
1b = sucB 0b

add1 : Bin⁺ → Bin⁺
add1 = addCarryToBitList 1b

data Positive : Bin⁺ → Set      -- "ends with 1"  
  where			
  single : Positive (1b ∷ [])
  cons   : {b : Bit} → {bs : Bin⁺} → Positive bs → Positive (b ∷ bs)

test : Bit → Bit            -- testing  (sucB (sucB ()))
test 0b               = 0b
test (sucB 0b)        = 0b
test (sucB (sucB ()))

positive-add1 : {bs : Bin⁺} → Positive bs → Positive (add1 bs)

positive-add1 {0b ∷ _}       (cons pos-bs) =  cons pos-bs
positive-add1 {sucB 0b ∷ []} single        =  cons single
positive-add1 {sucB 0b ∷ _}  (cons pos-bs) =  
                                           cons (positive-add1 pos-bs)
positive-add1 {sucB (sucB ()) ∷ _}
--------------------------------------------------------------------

1. Agda always insists on the presence of the pattern  sucB (sucB _),  
as if it does not see that it is not in  Bit = Fin 2.

2. All right, I use the pattern  (sucB (sucB ()))  to eliminate the
case.  
This does work in `test', and also in the version of  positive-add1' --
which has  bs  as explicit.
But it is not type-checked in the `implicit' version.  

Thank you in advance for explanation,

------
Sergei