[Agda] Induction-induction in a tricky order

[Dr. ERDI Gergo]

On Tue, 15 Mar 2016, Simon Boulier wrote:

> Is it a way to type check the following:
>       data Foo  : Set
>       data Bar  : Foo → Set
>       data Bar2 : Foo → Set
>
>       data Foo where
>         foo   : (x : Foo) → Bar x → Bar2 x → Foo
...

If you put them in a 'mutual' block, that should be OK (as long as 
positivity blah blah blah).