Assuming countable choice, every countably compact paracompact Hausdorff space is compact

Let $\mathcal{U}$ be an arbitrary open cover, and take a locally finite open refining cover $\mathcal{V}$ by [F2].

Suppose $\mathcal{V}$ were infinite. For every $n$ the family of $(n+1)$-element subsets of $\mathcal{V}$ is nonempty; [A1] chooses one $E_n$. Then $E={\bigcup }_n{E}_n$ is at most countable by [L2] and infinite because it has finite subsets of arbitrarily large size. Hence, by the definition of at-most-countable, $E$ is countably infinite; enumerate its distinct members as $(V_n{)}_{n\in \mathbb{N}}$.

By [A1] choose $d_n\in V_n$ for every $n$. The range $D=\{d_n:n\in \mathbb{N}\}$ is infinite: if it were finite, local finiteness would make only finitely many distinct $V_n$ meet $D$, but every $V_n$ contains $d_n\in D$. Moreover the singleton family $\{\{d\}:d\in D\}$ is locally finite, since a neighbourhood meeting only finitely many $V_n$ can contain only finitely many points $d\in D$.

Hausdorffness makes points closed, so [L1] makes $D$ closed. For each $d\in D$, local finiteness gives a neighbourhood meeting only finitely many points of $D$; pass to an open subneighbourhood and remove those finitely many other closed points. Using [A1] along an enumeration of $D$ yields open sets $O_d$ with $O_d\cap D=\{d\}$.

The open set $X\setminus D$, together with the at most countable family $\{O_d:d\in D\}$, is an open cover with no finite subcover, contradicting countable compactness in [F1].

Hence $\mathcal{V}$ is finite. By [L3], select for each member of this finite refining family one containing member of $\mathcal{U}$; the selected members form a finite subcover of $\mathcal{U}$.

Since $\mathcal{U}$ was arbitrary, [F1] proves that $X$ is compact.