[Agda] difficulties with patterns

[Sergei Meshveliani]

Please,
how can one avoid difficulties in using patterns?
(what is a common way out?).

For example, this program works:

 hasLast1-toBDigs-suc-n : (n : ℕ) → HasLast1 $ toBDigs $ suc n
 hasLast1-toBDigs-suc-n n =
             cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs 
    where
    pr             = toBDigits n 
    bs             = proj₁ pr          
    hasLast1-if-bs = proj₂ $ proj₂ pr         

    digs-n'          = toBDigs $ suc n
    digs-n'=addC1-bs = toBDigs-suc-eq {n}

    hasLast1-addC1-bs : HasLast1 $ addC1 bs
    hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs


Then I try to improve the style and replace the three assignments and
projections with pattern matching:

    case toBDigits n
    of \
    { (bs , (_ ,  hasLast1-if-bs)) →
            let
               digs-n'          = toBDigs $ suc n
               digs-n'=addC1-bs = toBDigs-suc-eq {n}

               hasLast1-addC1-bs : HasLast1 $ addC1 bs
               hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
            in
           cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
    }

And obtain the report 

  bs != (proj₁ (.Int.Bin2._.toBits n n n (≤refl PE.refl)))  
  of type  (List Bit)
  when checking that the expression  hasLast1-addC1-bs  has type
  HasLast1 (addC1 (toBDigs n)).

The checker somehow does not allow to improve style.

Thanks,

------
Sergei