Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
I'll repeat what szany and xyzzy123 mentioned: you work at a level of abstraction where infinite data structures are represented symbolically with enough definitional scaffolding to allow proofs to go through.
In a sense, a properly typed program provides a proof of some theorem over infinite data structures. For instance, an instance of a tree (in generic Java) is usually a finite data structure, but the set of all trees representable in Java is infinite. (Handwaving begins) The types prove that certain operations can't happen, like a tree of Strings changing to a tree of Arrays by a node search algorithm, which is a proof about an infinite set.