How to Prove Type Soundness of Java-like Languages Without Forgoing Big-step Semantics