prove remaining cheats in patLangProof
update some do_app_cases theorems