Internalize Nat in example
Generic elim with implicit type parameter arguments.
Add back generic eliminators in Darkwing, now improved with generic motives.