progress on semantics of VSUBST

based on ideas from and a few hours of pair-proving with Magnus
delete mostly-probably-junk at end of sholSemanticsScript.sml
start trying to fill the cheats in VSUBST_dbVSUBST