[Agda] redefining a value for `with'

[Sergei Meshveliani]

Dear all,

The proof for  ineq  below uses the witness  leq  in the line (II).
And Agda2.5.4  reports that  leq  in the line (II) has not the needed
type.
Then, I add a parasitic definition  leq'  in the line (I), 
and replace leq with leq' in the line (II).
And this latter program is type-checked.

----------------------------------------------------------
  aux :  ∀ a cnt → log' a ≤' cnt → Foo 
  ...
  aux (suc2* a) (1+ cnt) leq =  foo
    where
    a' = suc2* a

    leq' :  log' a' ≤' 1+ cnt
    leq'  = leq                    -- (I)

    ineq :  log' a ≤' cnt
    ineq with a ≟ 0#
    ... | yes a≡0 =  ...
    ... | no a≢0  =
          ≤'begin log' a             ≡≤'[ refl ]
                  ... 
                  pred' (log' a')     ≤'[ NatP.pred-mono leq ]   -- (II)
                                                      -- leq'
                  pred' (1+ cnt)     ≡≤'[ refl ]
                  cnt
          ≤'end
-----------------------------------------------------


1) Is this a bug in Agda?
2) I wonder how to avoid this parasitic definition of leq'.

I could reduce the example to a self-contained one, but I do not know,
may be you can tell of it as it is.

Thanks,

------
Sergei