inductive predicates

Feb 10 at 1:19 PM
Edited Feb 10 at 1:21 PM
I guess that Dafny syntax doesn't allow to declare auxiliary variables in the body of inductive predicates, does it? why?