[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

Jan Burse schrieb:
>
> Or what would be the mild condition on R
> to make the inference rule meaningful?

Ramana Kumar just wrote me:
 > The condition is that R does not mention any
 > variables assigned in C.

Then I also wonder how this is related to choice
principles. I see that it is related to variable
occurence rules. So if I desugar the following:

    { P } C { Q }

I get:

    P(x,z) -> forall y (C(x,y) -> Q(y,z))

Question is now whether this implies:

    P(x,z)&R(z) -> forall y(C(x,y) -> Q(y,z)&R(z))

I guess the answer is affirmative already in
minimal logic. But I might be also wrong here.

Bye