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.
Check out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: http://adam.chlipala.net/cpdt/html/Coinductive.html
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.