TransformerWithPaths now traverses Ensuring
DefaultTactic.generatePreconditions and generateCorrectnessConditions now looks in fullBody
Fix CodeGeneration to handle Require
Don't collect Require, Ensuring in collectCorrectnessConditions