[Agda] termination with `where'

[Sergei Meshveliani]

Dear Agda developers,

For a certain fragment of 

  f : (u v : Expression) -> foo u v ≈ foo' u v
  f (x :+ y) (e :* e') =
    begin
     ...    ≈[ +cong (aux x z)
                     (aux y z)   -- (I) 
             ]
     ...  
    ∎
    where z = e :* e'

Agda 2.6.0-207bde6  reports  "Termination checking failed ...", 
and marks yellow the call  (aux y z).

Replacing  (aux y z)  with   (aux y (e :* e'))  
satisfies the type checker.
Here  x, y, e, e'  are terms constructed with certain data
constructors  :0, :1, gen, _:+_, _:*_.

It looks strange that the termination checker is not stable under the
`where' construct.

What people think of this?

Regards,

------
Sergei