Kast in k

I created this diff for use in managing the discussion on the KORE syntax. We may choose to close it rather than merge it, I just need a place to put comments.
why no ensures? what if I want the definition to always start out assuming something is true?