Hereditary substitution in Dafny.

Quite painful compared to Agda, because of lack of indexed families.

Not much proofs, but at least, the normalizer terminates :)