move some theorems into miscTheory
update do_app_pat_correct