slow progress on semantics_VSUBST

went through various variations on the theorem statement. the result
in this commit is pretty similar to the original... the Abs case is left
and is the most difficult.