invert-app
cleanup
invert-wf-rec
sub-tp-refl no longer needed. need to fill in sub lemmas