[Agda] `with' in standard functions

[Sergei Meshveliani]

People,

There is a certain problem with user proofs for Standard library
functions that use `with' or `case_of_'.  
If a function is written without `with' (`with' replaced with calling an
auxiliary function  aux, and this  aux  is exported from the module),  
then it is much easier to compose various new proofs about it.

But the user cannot change implementation for a standard function. 

For example,  Data.Bin  implements 

-------------------------
fromBits : List Bit → Bin
fromBits []        = 0#
fromBits (b  ∷ bs) with fromBits bs
fromBits (b  ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
fromBits (0b ∷ bs) | 0#     = 0#
fromBits (1b ∷ bs) | 0#     = [] 1#
fromBits (⊥b ∷ bs) | _
-------------------------

I need to prove 

          fromBits-bs++1 :  fromBits ∘ (_∷ʳ 1b) ≗ _1#

And find it difficult.
Then I get free of `with', and a proof becomes plain and easy to
compose:

--------------------------------------------------
fromBits-aux : Bit → List Bit → Bin → Bin    -- needs to be exported

fromBits-aux b  bs (bs' 1#) = (b ∷ bs') 1#
fromBits-aux 0b bs 0#       = 0#
fromBits-aux 1b bs 0#       = [] 1#
fromBits-aux ⊥b bs _

fromBits' : List Bit → Bin
fromBits' []       = 0#
fromBits' (b ∷ bs) = fromBits-aux b bs (fromBits' bs)


fromBits-bs++1 :  fromBits' ∘ (_∷ʳ 1b) ≗ _1#
fromBits-bs++1 []       =  refl
fromBits-bs++1 (b ∷ bs) =
  begin
    fromBits' (b ∷ (bs ∷ʳ 1b))                        ≡⟨ refl ⟩
    fromBits-aux b (bs ∷ʳ 1b) (fromBits' (bs ∷ʳ 1b))
       	       	       	       	    ≡⟨ cong (fromBits-aux b (bs ∷ʳ 1b))
                                            (fromBits-bs++1 bs)
                                     ⟩
    fromBits-aux b (bs ∷ʳ 1b) (bs 1#)  	       	      ≡⟨ refl ⟩
    (b ∷ bs) 1#
  ∎
---------------------------------------------------

Please, what is a way out?

Thanks,

------
Sergei