invert-var-cases, not sure if it is useful, plus will require a new sub-tp/tbindx rule.
down to one lemma