parallel -> forall in Dafny...

... using custom Dafny at tip but keeping temporary hack for ghost alloc
and reverting principled fix which doesn't work with Dot6.