[Logiweb] Side conditions

[Frederik Eriksen]

Hi logiweb at diku.dk,

Suppose you've proven a lemma called "Lemma A" which has the form

SIDECOND-1 |= SIDECOND-2 |= (whatever Lemma A states)

where SIDECOND-1 and -2 are two side conditions. Suppose further that 
you want to use Lemma A to prove a lemma called "Lemma B". The side 
condition SIDECOND-1 happens to be necessarily true in the context of 
Lemma B; however, SIDECOND-2 is not necessarily true. Is there any way 
to prove

SIDECOND-2 |= (whatever Lemma B states)   ,

or will you have to make do with the weaker claim

SIDECOND-1 |= SIDECOND-2 |= (whatever Lemma B states) ?

Best Regards
Frederik Eriksen.