Dot3.dfy compatible with the latest Dafny release (modulo patch).

Use an explicit brain-dead step index for all type judgements. Not as
nice as before, since some statements that were auto-proved before now
need to be proved.

At least, no unsound use of co-predicates, like in Dot.dfy and Dot2.dfy,
which don't work with latest Dafny release.

Verifies without errors, though had to change some asserts to assumes
:/.