Fixed recursor for higher W-types.
Wrote induction principle for higher W-types. (Path computation rules are still missing, also for recursor...)