Existence Property for Heyting Arithmetic