```Inductive toto := | Toto : forall n, unit -> is_zero n = true-> toto.``` and ```Inductive toto := | Toto : forall n, is_zero n = true-> unit -> toto.``` are supported by `#[only(param1_trivial)] derive toto.` while ```Inductive toto := | Toto : unit -> forall n, is_zero n = true -> toto.``` is not.