The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/22/2014 05:55 PM, Nuno Gaspar wrote:
> Hello.
>
> Consider the following.
>
> Parameter set : list nat.
> CoInductive trace : LList nat -> Prop :=
>    | empty : trace LNil
>    | step  : forall l, exists n, In n set ->
>              trace l ->
>              trace  (LCons n l).
>
> The above does not typecheck, as the scope of the existential
> quantification goes up to the conclusion. Of course, if I put parentheses
> then variable n is no longer in scope...
>
> I want  to model the fact that I can pick any element from set, and include
> the picked element in the predicate conclusion..
>
> How would you go about this? :)
>
> Cheers.

It looks to me like merely replacing that "exists n" with "forall n" 
actually does what you describe.  Having "exists n" there says something 
like "Only certain n's in set that allows this trace to continue" 
instead of "Any (non-deterministic) n in set allows this trace to continue".

-- Jonathan