[SAL-HELP] axioms about a module

[Angelo Gargantini]

I have the following (part of) spec:

cruisecontrol: CONTEXT =     BEGIN
    main : MODULE = BEGIN
        INPUT  ignited: BOOLEAN
        INPUT  engRun: BOOLEAN
    END;
       
    % property for CC %%% replace with true
    tp : THEOREM main |- G( true);
END

I would like to add the assumption that when ignited is false, also 
engRun is false, and then prove properties starting from that assumption.
The only thing I can do now is to add a new BOOLEAN var and define:
DEFINITION invCruise = ignited => NOT engRun
And modify the theorem:
    tp : THEOREM main |- G(invCruise => true);

Is there a way to add the assertion at the level of context?
I tried to define a constant in the context (not in the module)
    invCruise = main!ignited => NOT main!engRun
but this is incorrect.
I was not able to use "OBLIGATION" either, which may be useless, since 
it is equivalent to THEOREM.
My question: what is the right way to introduce an assumption about a 
module and to use it when proving properties?
thanks

Angelo Gargantini
University of Bergamo  - Italy