[POPLmark] How to believe the Twelf proof of 1a

[Randy Pollack]

Karl,

I'm still unclear on the meaning of "var".  Suppose I want to believe
that the main formal result in file 1a.elf proves the intended
property of the intended object system.

  %block bind  : some {t:tp}
		 block {x:tp} {dv:var x} {d:assm x t} {thm:assm_var d dv}.
  trans : sub S Q -> sub Q T -> sub S T -> type.
  %mode trans +X1 +X2 -X3.
  - : trans D1 D2 D3 <- trans* _ _ nat_eq_ D1 D2 D3.
  %worlds (bind) (trans _ _ _).
  %total {} (trans _ _ _).

(You've pointed out that the world (bind) is part of the statement of
this result.)

I must believe some adequacy theorem about "sub" and "assm", which in
this case resides in the world

  some {t:tp} block {x:tp} {d:assm x t}

(As we have discussed, by choosing the world of the adequacy theorem,
I specify which of the possible object systems I'm interested in.
E.g. one could consider the world

  some {t:tp -> tp} block {x:tp} {d:assm x (t x)}  %% funny binding

but that is not the intended object system.)

QUESTION: what do I need to believe about "var" in order to believe
the theorem?  "var" doesn't show up in the declaration of "sub" or in
the adequacy theorem, but it does appear in the statement of "trans".

Randy