[POPLmark] Adequacy for LF

[Randy Pollack]

Karl Crary writes:
 > The central point is the definition of adequacy.  Following the original 
 > paper on LF, we say that an encoding is adequate exactly when it defines 
 > a bijection between constructs in the object language and canonical 
 > forms (of appropriate type in an appropriate context) in LF, and that 
 > bijection respects substitution.

What does "respects substitution" mean for the representation of
derivations of "sub" in file 1a.elf?

Randy