learn about polymorphism. huh, constructors take a type as an argument -- type as a first-class thing in Coq? still need to write and prove theorems in Lists.v