added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals

modernized syntax declarations, and make them actually work with authentic syntax;

observe standard convention for syntax consts;

proper type syntax (cf. 7425aece4ee3);