I would express the fact that $p$ lies in the set of programs with infinite domain $Inf$ as follows:
$$p\in Inf\iff\forall x\exists y > x \exists z T(p,y,z)\\ \iff \forall x\exists y(y > x \to \exists z T(p,y,z))\\ \iff \forall x\exists z\exists y(y > x\to T(p,y,z)) $$
but I've read somewhere that this property is expressed as $$p\in Inf\iff \forall x \exists z\exists y (y > x \land T(p,y,z))$$ and I believe these expressions aren't equivalent. Did I express this incorrectly then? I don't see anything wrong with my (first) expression.
You did express it incorrectly. The issue is in treating the bounded quantifiers - "$\forall$" and "$\exists$" behave quite differently:
"$\forall a<b(\varphi)$" is an abbreviation for "$\forall a(a<b\rightarrow\varphi)$."
"$\exists a<b(\varphi)$" is an abbreviation for "$\exists a(a<b\wedge\varphi)$."
Note that there is not an obvious notational "duality" here. It is still true however that the two bounded quantifiers are dual to each other in the sense that $$\neg\exists a<b\neg(\varphi) \quad\equiv\quad \forall a<b(\varphi)$$ and similarly $$\neg \forall a<b\neg(\varphi) \quad\equiv\quad \exists a<b(\varphi).$$ So this is a case where the logical notation we're used to actually makes it a little harder to remember what the abbreviations mean.