-

Inductive wf: envmode -> env typ -> env typ -> env val -> Prop :=
| wf_empty: forall m, wf m empty empty empty
| wf_push: forall m e1 e2 s x T v,
    wf m e1 e2 s ->
    x # e1 ->
    x # s ->
    ty_trm ty_precise sub_general (get_ctx m e1 e2) (get_sigma m e1 e2) (trm_val v) T ->
    wf m (e1 & x ~ T) e2 (s & x ~ v).

Definition wf_stack (G: ctx) (S: sigma) (s: stack): Prop :=
  wf env_stack G S s.

Definition wf_store (G: ctx) (S: sigma) (s: store): Prop :=
  wf env_store S G s.
    
Definition wf_stack_store(G: ctx) (S: sigma) (sta: stack) (sto: store): Prop := 
  wf_stack G S sta /\ wf_store S G sto.


Theorem wf_stack_ind
     : forall P : ctx -> sigma -> stack -> Prop,
       P empty empty empty ->
       (forall (G : ctx) (S : sigma) (s : stack) (x : var) (T : typ)
          (v : val),
        wf env_stack G S s ->
        P G S s ->
        x # G ->
        x # s ->
        ty_trm ty_precise sub_general G S (trm_val v) T ->
        P (G & x ~ T) S (s & x ~ v)) ->
       forall (c : ctx) (s : sigma) (s0 : stack), wf env_stack c s s0 -> P c s s0.
Proof.
...

Lemma ctx_binds_to_stack_binds_raw: forall stack G S x T,
  wf_stack G S stack ->
  binds x T G ->
  exists G1 G2 v, G = G1 & (x ~ T) & G2 /\ binds x v stack /\ ty_trm ty_precise sub_general G1 S (trm_val v) T.
Proof.
  introv Wf Bi. gen x T Bi. 
  refine (wf_stack_ind (* P *) (fun (G:ctx) (S:sigma) (stack0:stack) => 
  forall (x : var) (T : typ),
binds x T G ->
exists G1 G2 v,
G = G1 & x ~ T & G2 /\
binds x v stack0 /\ ty_trm ty_precise sub_general G1 S (trm_val v) T
)
  (* P0 *) _ (* P Ind *) _ Wf ); intros.
  + false* binds_empty_inv.
  ...