Progress on type soundness based free-var properties

Got it down to one technical lemma about the domains of weakened module
environments which is still cheated.  But several cheats removed form
replCorrect_lem.