starting a sketch of weakest pre-condition in Imp