cases-sub-tp -> cases-subeq-tp
invert-fun
wip on invert-wf-fun