[Agda] on `data' declaration

[Sergei Meshveliani]

People,

consider the declaration like 

 data Foo (c x y d : ℕ) :  Set
      where
      let e = c + (y * y + y)

      foo1 : x < e → Foo c x y d
      foo2 : x > e → (x ≡ e + d) → Foo c x y d
      foo3 : ...


Agda rejects it. And the programmer is forced to set several times the
expanded expression for  e  in several data constructors.

I wrote
 
 private expr =  \c y ->  c + (y * y + y)

 data Foo (c x y d : ℕ) :  Set
      where
      foo1 : x < expr c y → Foo c x y d
      foo2 : x > expr c y → (x ≡ (expr c y) + d) → Foo c x y d
      foo3 : ...

Can anybody, please, suggest any better way out?

Thanks,

------
Sergei