The Knuth-Bendix completion algorithm is used in computer algebra. Its proof of correctness relies on Kruskal's tree theorem, if I understand correctly. The proof of Kruskal's tree theorem is very nonconstructive: http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem