[Agda] "open" in record telescope

[mechvel at scico.botik.ru]

People,

I have

record Foo (R : FooFooFoo-Record)
            (open FooFooFoo-Record R using (Carrier; _≉_; 0#; Op)
            (op  : Op)
            (op' : (x : Carrier) → x ≉ 0# → Carrier) :  Set _
   where
   field ...


But Agda 2.6.1 does not allow `open' in the record telescope.
It is possible to write this as

record Foo
   (R   : FooFooFoo-Record)
   (op  : FooFooFoo-Record.Op R)
   (op' : (x : FooFoo-Record.Carrier R) → FooFoo-Record._≉_ x 
(FooFoo-Record.0# R) →
                                          FooFoo-Record.Carrier R) :
                                          Set _
   where
   field ...

Can this be expressed in a nicer form?

Thanks,

------
Sergei