Changed type reduction to perform substitutions according to ctx.
Changed pat-reduce to use reduction relation and added cases.