More about arrays: aloc are now per cell, loc_array is a union, WIP to prove modifies for upd
More about arrays: aloc are now per cell, loc_array is a union, WIP to prove modifies for upd

FStarLang/FStar,FStarLang/FStar,FStarLang/FStar