fix some broken proofs
first case of semantics_VSUBST

not completely sure about statement