Fix ARM examples for length-nil Part of #346
Renamed bsubst to update (as it is in v4T). Moved a few definitions/theorems to better homes.