[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