"Every finitely-branching tree with infinitely many nodes has an infinite branch" is constructively false, as witnessed by the following counterexample:
http://math.andrej.com/wp-content/uploads/2006/05/kleene-tree.pdfhttps://math.andrej.com/wp-content/uploads/2006/05/kleene-tree.pdf
Andrej Bauer's exposition (above) is especially nice; most textbooks take a far less direct route to the result, which makes it harder to see what's really going on past the level of "yeah, the proof is correct step-by-step."
