Coq isn't very good for developing with properties encoded in the types. Such properties are defined seperately from the data structures involved.