Yep, and you could even prove "nat" is isomorphic to the type of binary numbers "Bin := List (0 | 1)" and transport proofs there too.