Let $\mathrm{HA}$ denote ordinary first-order Heyting arithmetic in the language of natural numbers, without adding Church's Thesis as an axiom schema. Fix a standard arithmetic computation predicate $T(e,n,m)$ meaning that the program with index $e$ halts on input $n$ with output $m$. For an arithmetic formula $A(n,m)$, let $\mathsf{CT}_A$ be the schema instance \begin{align*} \bigl(\forall n\,\exists m\,A(n,m)\bigr)\to \exists e\,\forall n\,\exists m\,(T(e,n,m)\land A(n,m)). \end{align*} The full Church's Thesis schema is the collection of all such instances $\mathsf{CT}_A$. Ordinary $\mathrm{HA}$ does not prove this full schema.