Added the GameContract.

@bsoetaer 
More complete invariant would include that there are no empty spaces below a valid player token in a column. Could be done with each_with_index and assert that the i index conforms to number_of_tokens(j) 
i >= column_height - number_of_tokens(j) then t === 1..2