Weak weak Koenig and covering spaces

[Timothy Y. Chow]

Are any basic topological theorems about covering spaces unprovable in 
RCA_0?

The reason I ask is that I was recently refreshing my memory about some of 
those results, and it seems that some version of the Vitali covering lemma 
is typically used when lifting a map to a covering space.  So maybe the 
weak weak Koenig lemma is needed?

There are some basic results about finitely generated groups that have 
nice proofs using covering spaces.  Perhaps the simplest one is that a 
subgroup of a free group is free.  More sophisticated examples can be 
found in Serre's book "Trees."  Are any of these results unprovable in 
RCA_0?

Tim