The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> 1 subgoal
>
>   p' : Process
>   l : list Process
>   mw : list Package
>   H : forall p : Process,
>       In p l ->
>       exists a : Package,
>         In a mw /\
>         PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In n 
> (Y a))
>   ============================
>    exists m : list Package,
>      forall p : Process,
>      In p (p' :: l) ->
>      exists a : Package,
>        In a m /\
>        PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In n 
> (Y a))
>
> T < exists (Build_Package (PID p') ??????? :: mw).

Don't you just want to put [(X p')] in the blank?  I can't spot anything 
tricky going on here.

P.S.: Please don't include long proof interaction traces in future 
messages.  Showing one proof sequent would be enough for me, and I 
almost ignored your message because of how long it was.  (Others may 
have different opinions, but I'm guessing that most agree on this.)