Tail Merging in Ωmega

Today finally I got around improving my Cat-like language optimizer with a new twist:
I can finally factor out common instructions from the end of the two If legs and prepend them to the If's continuation. This wouldn't be an interesting achievement if it wouldn't be written in Ωmega's type-pedantic fragment. To wit:

• tailMerge False [If [Dup]l [Dup]l, Print]l (revThrist' [Dup]l) (revThrist' [Dup]l) [Print]l
• becomes: [(PopN 1v),Dup,Print]l : forall a (b:Prod *0).Thrist Cat [Bool,a; b]sh [a; b]sh

If you think the above lines are in Chinese, you can stop now. If you discover that the If has completely been eliminated and replaced by popping a boolean and duplicating the TOS, then you are pretty good in reading obscure code.
The funny thing is that all the types of values that are on the stack are painstakingly tracked, and the transformation is automatically type correct in Cat because it is type checked in the metalanguage.

I am sure that similar transformations have been proven type correct (and thus pretty correct) before, however I would like to know whether this particular optimization has been already formalized using expressive types.

The big surprise for me was the fact that writing down the transformation only needed a dozen lines of code, support functions included. Of course, my proof of concept only matches on Dup instructions, but the rest is basically boilerplate.

The second surprise is, that so far I did not need a single theorem declaration, an indication that either I am still in very shallow waters regarding the power of Ωmega's typechecker, or my Thrist construction is so clever that it provides enough type hints to the narrowing engine to deduce all types.

I am in the process of writing a paper on all this, and - as always - need some encouragement. Tail merging will definitely belong to the beef part of it.