When defined as a `val function` the postcondition of the program function
`make` is just `result = make n v`, referring to the logical function `make`.
But the equality cannot be proven because array equality is not defined.

To facilitate proofs about results of the program functions `make`, this
commit separates the definitions of the logical function from the program
function `make`, so that the postconditions of the program function `make`
refer to the properties of the resulting arrey.