vJ 是错的

E 具有和函数 spec 类似的模式。 E_valid 和 spec 的正确性类似，即对于任意的类型参数 A 和 with 变量 a，spec 都成立。

E : ∀ A: Type, A -> Prop := (fun A a => P a).
E_valid : Prop := ∀ A a, E A a.

之前的基于 vJ 的 eeval 是错的。 vJ 应该要依赖于类型变量的取值，但是之前的写法没有依赖。

expr : ∀ (n: nat), type n -> Type

eeval : ∀ {tJ n} (cJ: const_asgn tJ) (vJ: var_asgn tJ n) {t: type n} (e: expr t),
          option (∀ Ts: vec Type n, teval tJ t Ts)

例如，用这个写法来对 E 本身（而不是代入具体类型）求值的话：

E_expr : expr 1 Propₜ := EApp `P` (EVar "a").
vJ : var_asgn tJ 1
var_asgn tJ 1 ≡ ∀ (p: string * type 1),   (* 变量名和类型 *)
                  option (∀ Ts: vec Type 1, teval p.2 tJ Ts)

eeval vJ cJ E_expr 会需要 vJ ("a", TVar 1) : option (∀ Ts: vec Type 1, Ts[@1])，这在语义上是错误的。括号里的类型等价于 ∀ T: Type, T。

well-scoped expr 没问题

Ctx n : Type := list (type n).

expr : ∀ {n: nat}, Ctx n -> type n -> Type

eeval : ∀ (J: asgn tJ) {n} {t: type n} {Γ: Ctx n} (e: expr Γ t),
          option (∀ (Ts: vec Type n) (Vs: dlist ⟦⋅⟧ Γ), teval t tJ Ts).