List

If Nat is the most basic datatype, List is the next basic datatype.
#
List
After the definition, List taken a Type is a Type.
Let construct a List of "a", "b", "c", step by step.
#
About induction over List
#
length
#
append
#
map
#
reverse
Proving Theorems About Nat
Vector