fixing up Patterns.
dead code cleanup.
adding join_env, to be the inverse of split_env.
the actual theorem about expr_of_mpattern.
adding implicit arguments for Case and _mmatchAt
prove weakening + dead code elimination.
implicit arguments on join_env.