[POPLmark] Twelf question

[Randy Pollack]

Consider the following Twelf script:

   tp : type.  %name tp T.
   top	: tp.

   assm : tp -> tp -> type.
   var  : tp -> type.

   %block rblock : some {t:tp}
		   block {x:tp} {d: assm x t} {v:var x}.

   assm_var : assm T _ -> var T -> type.
   %mode assm_var +X1 -X2.
   %worlds (rblock) (assm_var _ _).
   %total {} (assm_var _ _).

Twelf gives an error message:

   Coverage error --- missing cases:
   {T1:tp} {#rblock:{x:tp} {d:assm x T1} {v:var x}} {X1:var #rblock_x}
      |- assm_var #rblock_d X1.

I guess it means `since you allow a block containing "assm x T1" you
are required to produce a proof of "var x"'.  How can I express that I
want Twelf to use the proof "var x" from the same block?

Randy