Builtin Types Viewed as Inductive Families