[Agda] using (Acc _<_)

[Sergei Meshveliani]

Dear all, 

I wonder why the version II below is not type-checked:

--------------------------------------------------
{-# OPTIONS --termination-depth=2 #-}

foo :  (x : Bin) (nz : x ≢ 0#) → Acc _<_ x →
                           let 2x≢0 = x≢0⇒2x≢0 nz
                           in
                           2* x < 2^ (1+ (log₂ (2* x) 2x≢0))

foo 0#       nz   _           =  contradiction refl nz
foo (2suc x) x'≢0 (acc wf-x') =                               
      	       	   -- acc-x'  -- II
  ...
  where
  sx    = suc x;           x' = 2suc x
  2x'≢0 = x≢0⇒2x≢0 x'≢0;   2sx≢0 = x≢0⇒2x≢0 suc≢0;   sx<x' = suc<2suc x

  -- acc-sx : Acc _<_ sx                    -- II
  -- acc-sx = acc-2suc⇒acc-suc acc-x'

  lt0 :  2suc x < 2^ (log₂ (2* (2suc x)) 2x'≢0)
  lt0 =
   begin
    2suc x                           ≡[ 2suc-as∘ x ]
    2* sx                            <[ foo sx suc≢0 (wf-x' _ sx<x')
                                                     -- acc-sx  -- II
                                      ]
    ...

   ∎
-----------------------------------------------------

The code is not self-contained, but I hope, Agda developers can explain
the effect.

Here  foo  is applied recursively to the argument  sx,  which is smaller
than x'. 
There are three places marked with "II".
The version II is produced by
* changing  (acc wf-x')  to the variable  acc-x'  at the first place,
* un-commenting acc-sx,
* replacing (wf-x' _ sx<x') with  acc-sx.

The version (I) is type-checked, while for the version II it is reported
"Termination failed ...". 

This contradicts to that  acc-sx  has the needed type  Acc _<_ sx.

Is this a bug in Agda (version 2.6.0-05e8112) ?

Regards,

------
Sergei