[proofplan]
Apply dyadic bar compactness to the decidable bar $B$. This gives a level $N$ at which every depth-$N$ dyadic interval has an initial segment already certified by a finite witness set. There are only finitely many words of length $N$, so the union of their witness sets is finite. The depth-$N$ dyadic intervals cover $[a,b]$, and each one is contained in its certified ancestor interval, so the union of the corresponding finite families covers all of $[a,b]$.
[/proofplan]
[step:Apply dyadic bar compactness]
The predicate $B$ is decidable by hypothesis, and the same hypothesis says that $B$ is a bar on the binary tree. The dyadic bar compactness principle therefore gives a natural number $N$ such that every word $t \in 2^N$ has an initial segment $s \preceq t$ with $B(s)$.
[guided]
The theorem assumes that $B \subseteq 2^{<\mathbb{N}}$ is decidable and that every infinite binary sequence has an initial segment $s$ satisfying $B(s)$. Applying dyadic bar compactness to this decidable bar gives one number $N$ with the following uniform property: for every word $t \in 2^N$, some prefix $s \preceq t$ satisfies $B(s)$.
[/guided]
[/step]
[step:Choose certified ancestors at the uniform level]
Fix a word $t \in 2^N$. Among the finitely many prefixes of $t$, search in increasing length until the first prefix $s_t$ with $B(s_t)$ is found. This search terminates because the previous step gives at least one such prefix, and it is effective because $B$ is decidable. Since $s_t \preceq t$, the depth-$N$ interval satisfies $I_t \subseteq I_{s_t}$.
By the witness-data hypothesis, $B(s_t)$ supplies a finite set $F_{s_t} \subseteq I$ such that $(U_i)_{i \in F_{s_t}}$ covers $I_{s_t}$. Hence the same finite family covers $I_t$.
[guided]
For each fixed $t \in 2^N$, its prefixes form the finite list of words of lengths $0,\ldots,N$. Since $B$ is decidable and at least one prefix satisfies $B$, a finite search chooses a first such prefix $s_t \preceq t$. The inclusion $s_t \preceq t$ gives $I_t \subseteq I_{s_t}$. The witness data attached to $B(s_t)$ gives a finite set $F_{s_t} \subseteq I$ whose family $(U_i)_{i \in F_{s_t}}$ covers $I_{s_t}$, hence also covers $I_t$.
[/guided]
[/step]
[step:Assemble one finite subcover]
There are finitely many binary words of length $N$. Define
\begin{align*}
F = \bigcup_{t \in 2^N} F_{s_t}.
\end{align*}
This is a finite subset of $I$, because it is a finite union of finite subsets of $I$.
The level-$N$ dyadic intervals cover the original interval:
\begin{align*}
[a,b] = \bigcup_{t \in 2^N} I_t.
\end{align*}
Let $x \in [a,b]$. Choose a word $t \in 2^N$ with $x \in I_t$. The previous step shows that $(U_i)_{i \in F_{s_t}}$ covers $I_t$, so $x \in U_i$ for some $i \in F_{s_t}$. Since $F_{s_t} \subseteq F$, the point $x$ lies in a member of $(U_i)_{i \in F}$.
[guided]
The set $2^N$ of binary words of length $N$ is finite, and each $F_{s_t}$ is finite, so $F=\bigcup_{t \in 2^N} F_{s_t}$ is finite. Since $[a,b]=\bigcup_{t \in 2^N} I_t$, every $x \in [a,b]$ lies in some $I_t$. For that $t$, the family $(U_i)_{i \in F_{s_t}}$ covers $I_t$, so $x \in U_i$ for some $i \in F_{s_t} \subseteq F$. Therefore $(U_i)_{i \in F}$ covers every point of $[a,b]$.
[/guided]
[/step]
[step:Conclude Heine-Borel compactness]
The finite set $F \subseteq I$ constructed above has the property that every $x \in [a,b]$ lies in some $U_i$ with $i \in F$. Therefore $(U_i)_{i \in F}$ is a finite subcover of $[a,b]$, as required.
[/step]
