Work on patLangProof

Completely replaced the proof of do_app_pat_correct as this was easier
than understanding the previous proof. do_app_pat_v_pat is cheated, but
everything else works in patLangProof.