Coq 中 witness 列表的表示

context 中的变量怎么表示？

void f()
/*@ With t
    Require t % 4 == 0
    Ensure  emp */
{
  //@ t % 2 == 0
}
// Witness: forall t, t % 4 == 0 -> t % 2 == 0

Soundness 是否需要感知到 Given 的存在？

(* Old, wrong *)
entail_wit : list {n: nat & (Assertion n * Assertion n)%type};
(* New? *)
entail_wit : list {n: nat & list (var_name * type n) * (Assertion n * Assertion n)%type};
(*                 Types    Vars                        pre           post *)

Definition var_asgn (tJ: type_asgn) n (Ts: vec Type n) : Type :=
  forall (p: var_name * type n), option (teval tJ (snd p) Ts).

eeval tJ (cJ: const_asgn tJ) n (Ts: vec Type n) (vJ: var_asgn tJ n Ts)
      (t: type n) (e: expr t) : option (teval n tJ t).

eeval tJ (cJ: const_asgn tJ)
      (n: nat)                      (Ts: vec Type n)
      (l: list (var_name * type n)) (Vs: dlist (λ p, teval n tJ p.2) l)
      (*                            (Vs: dlist (λ p, option (teval n tJ p.2)) l) *)
      (t: type n) (e: expr t) : option (teval n tJ t).

(* Substitution lemma? *)
⟦e (u ↦ v)⟧ vJ  =  ⟦e⟧ (vJ (u ↦ ⟦v⟧ vJ))
⟦e (u ↦ v)⟧ l Vs  =  match (find v in l Vs) in
                      | Some val => ⟦e⟧ (u :: l) (val ::: Vs)
                      | None => ⟦e⟧ l Vs
                      end
⟦e (u ↦ v)⟧ l Vs  =  ⟦e⟧ (u :: l) (find v in l Vs ::: Vs)

find tJ n (v: var_name * type n) l Vs : option (teval n tJ v.2)