Proof of weak normalization property in STLC