Fixing issue 997

fixed https://github.com/kframework/k/issues/997

There are three problems here:
1) KItem built from KLabelInjection and empty KList should have exact sort ```KItem```;
2) when we use the unification-based rewrite engine to execute programs, usually the resulting constraint should be a proper order-sorted substitution (except ```logik```). However, I cannot know whether the user is trying to just execute programs;
3) see https://github.com/kframework/k/issues/1003.

Basically, I fixed the first one and created an issue for the third one. I can also fix the second problem if there is an option that user can specify to tell the unification-based rewrite engine to check whether the resulting constraint should be a proper substitution. However, this is kind of redundant because the user can always just specify ```--pattern-matching``` to use the fast rewriter based on pattern matching.

@dwightguth @andreistefanescu please review