fix broken proof
delete semantics_aconv, reprove semantics_vfree_in

renamed the latter to semantics_fvs.
don't need aconv because it's just equality on de Bruijn terms.