Progress Theorem for the Simply Typed Lambda Calculus