In chunnel.pvs I have, for instance, a theory 'points' which defines a type 'points_value' and an assumption on this type 'points_ax'. In the theory 'Thedford_scenario' a constant 'mp' of type 'points_value' is declared and instantiated. I thought that this would then incur an obligation to prove the assumption 'points_ax'. However, on doing a typecheck no such tcc occurs. Why is this? Is there any other way to write this so that the relevant tcc's occur? Richard.