[POPLmark] Proof of progress

[Jerome Vouillon]

In lemma A.15 of the paper proof, case T-Let (t = let p=t1 in t2),
subcase "t1 is a value", you write:
   "Then t ---> match(p,t1)t2 by E-LetV".

Isn't this a bit fast?  It does not seem obvious to me from the proof
that match(p,t1)t2 is indeed defined.

-- Jerome