forbid extending sort K in the Java backend

Fixed https://github.com/kframework/k/issues/708

@dwightguth @radumereuta please review

So if we make it `KItem` it needs to be 

    syntax KItem ::= KItem "[" KItem "/" KItem "]"

because we don't want .K in the first position (`.K [ 3 / X ]` should evaluate to `.K`) or in the second position (`X[.K/X]` should evaluate to `.K`), and we don't ever want .K in the third position.

I would personally be in favor of that, and disallow applying substitution on .K