removed an assume in array-realized.fst...replaced with a definition