diff --git a/theories/context_inference.v b/theories/context_inference.v
new file mode 100644
index 00000000..b11aa25e
--- /dev/null
+++ b/theories/context_inference.v
@@ -0,0 +1,214 @@
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool eqtype seq.
+From compcert Require lib.Floats.
+From Wasm Require Export common typing operations.
+From Coq Require Import BinNat.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Section Context_inference.
+
+Variable host_function : eqType.
+
+Let function_closure := function_closure host_function.
+Let store_record := store_record host_function.
+
+Definition func_typing_inf (fs: list function_closure) (n: nat) : option function_type :=
+  option_map cl_type (List.nth_error fs n).
+
+Definition funcs_typing_inf (s: store_record) (inst: instance) : option (list function_type) :=
+  those (map (fun i => func_typing_inf s.(s_funcs) i) inst.(inst_funcs)).
+
+(* Choosing the most lenient bound *)
+Definition tab_typing_inf (ts: list tableinst) (n: nat) : option table_type :=
+  match List.nth_error ts n with
+  | Some _ => Some (Build_table_type (Build_limits 0%N None) ELT_funcref)
+  | _ => None
+  end.
+
+Definition tabs_typing_inf (s: store_record) (inst: instance) : option (list table_type) :=
+  those (map (fun i => tab_typing_inf s.(s_tables) i) inst.(inst_tab)).
+
+(* Choosing the most lenient bound *)
+Definition mem_typing_inf (ms: list memory) (n: nat) : option memory_type :=
+  match List.nth_error ms n with
+  | Some _ => Some (Build_limits 0%N None)
+  | _ => None
+  end.
+
+Definition mems_typing_inf (s: store_record) (inst: instance) : option (list memory_type) :=
+  those (map (fun i => mem_typing_inf s.(s_mems) i) inst.(inst_memory)).
+
+Definition global_typing_inf (gs: list global) (n: nat) : option global_type :=
+  match List.nth_error gs n with
+  | Some g => Some (Build_global_type g.(g_mut) (typeof g.(g_val)))
+  | _ => None
+  end.
+
+Definition globals_typing_inf (s: store_record) (inst: instance) : option (list global_type) :=
+  those (map (fun i => global_typing_inf s.(s_globals) i) inst.(inst_globs)).
+
+Definition inst_typing_inf (s: store_record) (inst: instance) : option t_context :=
+  match funcs_typing_inf s inst with
+  | Some fts =>
+      match tabs_typing_inf s inst with
+      | Some tts =>
+          match mems_typing_inf s inst with
+          | Some mts =>
+              match globals_typing_inf s inst with
+              | Some gts =>
+                  Some (Build_t_context inst.(inst_types) fts gts tts mts nil nil None)
+              | _ => None
+              end
+          | _ => None
+          end
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Definition frame_typing_inf (s: store_record) (f: frame) : option t_context :=
+  match inst_typing_inf s f.(f_inst) with
+  | Some C => Some (upd_local C ((map typeof f.(f_locs)) ++ tc_local C))
+  | None => None
+  end.
+
+Lemma func_typing_inf_agree: forall xs n x,
+    (func_typing_inf xs n == Some x) = 
+      functions_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold func_typing_inf, functions_agree.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth; rewrite Hnth => /=.
+  - assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+    move/ltP in Hlen.
+    by rewrite Hlen.
+  - cbn.
+    by lias.
+Qed.
+
+Lemma tab_typing_inf_agree: forall xs n x,
+    tab_typing_inf xs n = Some x ->
+    tabi_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold tab_typing_inf, tabi_agree, tab_typing, limit_match.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth => //=.
+  assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+  move => Hinf.
+  move/ltP in Hlen.
+  rewrite Hlen => /=.
+  injection Hinf as <-.
+  cbn.
+  rewrite Bool.andb_true_r.
+  apply/N.leb_spec0.
+  by lias.
+Qed.
+
+Lemma mem_typing_inf_agree: forall xs n x,
+    mem_typing_inf xs n = Some x ->
+    memi_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold mem_typing_inf, memi_agree, mem_typing, limit_match.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth => //=.
+  assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+  move => Hinf.
+  move/ltP in Hlen.
+  rewrite Hlen => /=.
+  injection Hinf as <-.
+  cbn.
+  rewrite Bool.andb_true_r.
+  apply/N.leb_spec0.
+  by lias.
+Qed.
+
+Lemma global_typing_inf_agree: forall xs n x,
+    (global_typing_inf xs n = Some x) ->
+    globals_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold global_typing_inf, globals_agree, global_agree.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth => //=.
+  assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+    move/ltP in Hlen.
+    rewrite Hlen => /=.
+    move => [<-] => /=.
+    apply/eqP; f_equal.
+    by lias.
+Qed.
+
+Lemma those_all2_impl {X Y Z: Type}: forall (xs: list X) (ns: list Y) (ts: list Z) (f: list X -> Y -> option Z) (g: list X -> Y -> Z -> bool),
+    (forall xs n x, f xs n = Some x -> g xs n x) ->
+    (those (map (f xs) ns) = Some ts) ->
+    all2 (g xs) ns ts.
+Proof.
+  setoid_rewrite <- those_those0.
+  move => xs.
+  elim => //=; first by intros; destruct ts.
+  move => y ys IH ts f g Heq Himpl.
+  remove_bools_options.
+  apply Heq in Hoption.
+  eapply IH in Hoption0; last by apply Heq.
+  by rewrite Hoption Hoption0.
+Qed.
+  
+Lemma funcs_typing_inf_agree: forall s inst xts,
+  (funcs_typing_inf s inst = Some xts) ->
+  all2 (functions_agree s.(s_funcs)) inst.(inst_funcs) xts.
+Proof.
+  move => f inst xts Hinf.
+  unfold funcs_typing_inf in Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  rewrite <- func_typing_inf_agree.
+  by apply/eqP.
+Qed.
+
+Lemma tabs_typing_inf_agree: forall s inst xts,
+  (tabs_typing_inf s inst = Some xts) ->
+  all2 (tabi_agree s.(s_tables)) inst.(inst_tab) xts.
+Proof.
+  move => f inst fts Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  by apply tab_typing_inf_agree.
+Qed.
+
+Lemma mems_typing_inf_agree: forall s inst xts,
+  (mems_typing_inf s inst = Some xts) ->
+  all2 (memi_agree s.(s_mems)) inst.(inst_memory) xts.
+Proof.
+  move => f inst fts Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  by apply mem_typing_inf_agree.
+Qed.
+
+Lemma globals_typing_inf_agree: forall s inst xts,
+  (globals_typing_inf s inst = Some xts) ->
+  all2 (globals_agree s.(s_globals)) inst.(inst_globs) xts.
+Proof.
+  move => f inst fts Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  by apply global_typing_inf_agree.
+Qed.
+
+Lemma inst_typing_inf_impl: forall s inst C,
+    inst_typing_inf s inst = Some C ->
+    inst_typing s inst C.
+Proof.
+  move => s inst C Hinf.
+  unfold inst_typing_inf in Hinf.
+  destruct inst.
+  remove_bools_options => /=.
+  apply/andP; split; last by apply mems_typing_inf_agree in Hoption1.
+  apply/andP; split; last by apply tabs_typing_inf_agree in Hoption0.
+  apply/andP; split; last by apply globals_typing_inf_agree in Hoption2.
+  apply/andP; split; last by apply funcs_typing_inf_agree in Hoption.
+  by apply/eqP.
+Defined.
+  
+End Context_inference.
diff --git a/theories/instantiation_sound.v b/theories/instantiation_sound.v
index 2f72a552..631c0b1f 100644
--- a/theories/instantiation_sound.v
+++ b/theories/instantiation_sound.v
@@ -92,7 +92,6 @@ Proof.
     by rewrite -> H.
 Qed.
 
-
 Let cl_type_check_single := @cl_type_check_single host_function.
 
 Lemma cl_type_check_single_aux s_funcs s_tables s_mems s_globals func funcs tabs mems globs:
@@ -111,7 +110,7 @@ Proof.
     rename H4 into Hinst_typing. rename H8 into Hbe_typing.
     apply cl_typing_native
       with (C := C)
-           (C' := upd_local_label_return C (tc_local C ++ t1s ++ ts) ([::t2s] ++ tc_label C) (Some t2s))
+           (C' := upd_local_label_return C (t1s ++ ts) ([::t2s]) (Some t2s))
           => //=.
     destruct C.
     rewrite /inst_typing. simpl.
@@ -630,10 +629,10 @@ Proof.
      this is no longer true in the future. *)
   exists (ET_tab {| tt_limits := {| lim_min := N.of_nat (tab_size tab); lim_max := table_max_opt tab |} ; tt_elem_type := ELT_funcref |}).
   econstructor; eauto.
-  unfold tab_typing => /=.
-  apply/andP; split => //.
-  rewrite nat_bin.
-  by lias.
+  unfold tab_typing, limit_match => /=.
+  apply/andP; split => //=; first by apply/N.leb_spec0; lias.
+  destruct (table_max_opt tab) eqn:Hopt => //.
+  by apply/N.leb_spec0; lias.
 Qed.
 
 Lemma ext_typing_exists_mem addr s:
@@ -648,12 +647,12 @@ Proof.
   destruct Hnth as [mem Hnth].
   
   (* Similar to tab_typing *)
-  exists (ET_mem {| lim_min := N.of_nat (mem_size mem); lim_max := mem_max_opt mem |}).
+  exists (ET_mem {| lim_min := mem_size mem; lim_max := mem_max_opt mem |}).
   econstructor; eauto.
-  unfold mem_typing => /=.
-  apply/andP; split => //.
-  rewrite nat_bin N2Nat.id.
-  by apply N.leb_refl.
+  unfold mem_typing, limit_match => /=.
+  apply/andP; split => //=; first by apply/N.leb_spec0; lias.
+  destruct (mem_max_opt mem) eqn:Hopt => //.
+  by apply/N.leb_spec0; lias.
 Qed.
 
 Lemma ext_typing_exists_glob addr s:
@@ -667,8 +666,6 @@ Proof.
     apply nth_error_Some in Hnth'; by lias. }
   destruct Hnth as [glob Hnth].
   
-  (* Note that all tables can be tab_typed. This lemma needs more information if
-     this is no longer true in the future. *)
   exists (ET_glob {| tg_mut := g_mut glob; tg_t := typeof (g_val glob) |}).
   econstructor; eauto.
   unfold global_agree => /=.
@@ -1045,9 +1042,13 @@ Proof.
                
                destruct tt. destruct tt_limits. simpl.
                rewrite /tab_typing. simpl.
-               apply/andP. split => //=.
-               rewrite /tab_size. simpl. 
-               by rewrite repeat_length.
+               apply/andP. split => /=.
+               - rewrite /tab_size. simpl. 
+                 rewrite repeat_length.
+                 apply/N.leb_spec0.
+                 by rewrite nat_bin N2Nat.id; lias.
+               - destruct lim_max => //.
+                 by apply/N.leb_spec0; lias.
              }
     -- (* memi_agree *)
       rewrite <- Forall2_all2 => /=.
@@ -1090,7 +1091,7 @@ Proof.
 
            destruct mt. 
            rewrite /mem_typing. simpl.
-           apply/andP. split => //=.
+           apply/andP. split => //=; last by destruct lim_max => //; apply/N.leb_spec0; lias.
            rewrite /mem_size /operations.mem_length /memory_list.mem_length. simpl.
            destruct lim_min => //.
            rewrite /page_size. simpl.
diff --git a/theories/instantiation_spec.v b/theories/instantiation_spec.v
index d4d2a6f9..730fa6d0 100644
--- a/theories/instantiation_spec.v
+++ b/theories/instantiation_spec.v
@@ -275,8 +275,8 @@ Definition module_func_typing (c : t_context) (m : module_func) (tf : function_t
     tc_global := c.(tc_global);
     tc_table := c.(tc_table);
     tc_memory := c.(tc_memory);
-    tc_local := c.(tc_local) ++ tn ++ t_locs;
-    tc_label := tm :: c.(tc_label);
+    tc_local := tn ++ t_locs;
+    tc_label := [::tm];
     tc_return := Some tm;
   |} in
   typing.be_typing c' b_es (Tf [::] tm).
diff --git a/theories/interpreter_ctx.v b/theories/interpreter_ctx.v
index df8f57cd..6055cb81 100644
--- a/theories/interpreter_ctx.v
+++ b/theories/interpreter_ctx.v
@@ -734,7 +734,7 @@ Proof.
         inversion Hftype as [s' i tvs C f Hit Hfi Hlocs]; subst.
         destruct fc as [fvs fk ff fes]; simpl in *.
         apply inst_t_context_local_empty in Hit; rewrite -> Hit in *; simpl in *.
-        rewrite length_is_size size_map -length_is_size in H3_getlocal; by lias.
+        rewrite cats0 length_is_size size_map -length_is_size in H3_getlocal; by lias.
 
     - (* AI_basic (BI_set_local j) *)
       get_cc ccs.    
@@ -753,7 +753,7 @@ Proof.
           inversion Hftype as [s' i tvs C f Hit Hfi Hlocs]; subst.
           destruct fc as [fvs fk ff fes]; simpl in *.
           apply inst_t_context_local_empty in Hit; rewrite -> Hit in *; simpl in *.
-          rewrite length_is_size size_map -length_is_size in H3_setlocal; by lias.
+          rewrite cats0 length_is_size size_map -length_is_size in H3_setlocal; by lias.
 
     - (* AI_basic (BI_tee_local j) *)
       destruct vs0 as [|v vs0].
diff --git a/theories/interpreter_func.v b/theories/interpreter_func.v
index a1d99caf..936a97dd 100644
--- a/theories/interpreter_func.v
+++ b/theories/interpreter_func.v
@@ -1917,6 +1917,7 @@ Proof.
     last by apply inst_t_context_local_empty in Hitype'.
   replace (tc_label C''') with ([::] : seq (seq value_type)) in Hetype;
     last by apply inst_t_context_label_empty in Hitype'.
+  rewrite cats0 in Hetype.
   by apply Hetype.
 Qed.
 
diff --git a/theories/type_preservation.v b/theories/type_preservation.v
index da77ab93..e554db84 100644
--- a/theories/type_preservation.v
+++ b/theories/type_preservation.v
@@ -787,13 +787,20 @@ Proof.
   move => m m' y Htype Hext.
   unfold mem_typing in *.
   unfold mem_extension in Hext.
-  remove_bools_options.
-  apply/andP; split; last by apply/eqP; rewrite -H2 -H0.
-  { apply/N.leb_spec0.
-    move/N.leb_spec0 in H.
+  unfold limit_match in *.
+  remove_bools_options; simpl in *.
+  - apply/andP; split => /=.
+    { move/N.leb_spec0 in H.
+      move/N.leb_spec0 in H1.
+      apply/N.leb_spec0.
+      by lias.
+    }
+    by rewrite - H0 Hoption0.
+  - move/N.leb_spec0 in H.
     move/N.leb_spec0 in H1.
+    rewrite Bool.andb_true_r.
+    apply/N.leb_spec0.
     by lias.
-  }
 Qed.
 
 Lemma mem_extension_C: forall sm sm' im tcm,
@@ -822,9 +829,19 @@ Proof.
   move => t t' y Htype Hext.
   unfold tab_typing in *.
   unfold tab_extension in Hext.
-  remove_bools_options.
-  apply/andP; split; last by apply/eqP; rewrite -H0; lias.
-  by lias.
+  unfold limit_match in *.
+  simpl in *.
+  remove_bools_options; cbn.
+  - apply/andP; split.
+    { move/N.leb_spec0 in H1.
+      apply/N.leb_spec0.
+      by lias.
+    }
+    by rewrite -H0.
+  - move/N.leb_spec0 in H1.
+    rewrite Bool.andb_true_r.
+    apply/N.leb_spec0.
+    by lias.
 Qed.
 
 Lemma tab_extension_C: forall st st' it tct,
@@ -1659,7 +1676,7 @@ Lemma t_preservation_vs_type: forall s f es s' f' es' C C' lab ret t1s t2s hs hs
     store_typing s' ->
     inst_typing s f.(f_inst) C ->
     inst_typing s' f.(f_inst) C' ->
-    e_typing s (upd_label (upd_local_return C (tc_local C ++ map typeof f.(f_locs)) ret) lab) es (Tf t1s t2s) ->
+    e_typing s (upd_label (upd_local_return C (map typeof f.(f_locs) ++ tc_local C) ret) lab) es (Tf t1s t2s) ->
     map typeof f.(f_locs) = map typeof f'.(f_locs).
 Proof.
   move => s f es s' f' es' C C' lab ret t1s t2s hs hs' HReduce HST1 HST2 HIT1 HIT2 HType.
@@ -1670,10 +1687,11 @@ Proof.
     replace [::BI_const v; BI_set_local i] with ([::BI_const v] ++ [::BI_set_local i]) in HType => //=.
     invert_be_typing.
     replace (tc_local C) with ([::]: list value_type) in *; last by symmetry; eapply inst_t_context_local_empty; eauto.
+    rewrite -> cats0 in *.
     rewrite H1.
     rewrite set_nth_map => //.
     by rewrite set_nth_same_unchanged.
-  - assert (exists lab' t1s' t2s', e_typing s (upd_label (upd_label (upd_local_return C (tc_local C ++ map typeof f.(f_locs)) ret) lab) lab') es (Tf t1s' t2s')); first eapply lfilled_es_type_exists; eauto.
+  - assert (exists lab' t1s' t2s', e_typing s (upd_label (upd_label (upd_local_return C (map typeof f.(f_locs) ++ tc_local C) ret) lab) lab') es (Tf t1s' t2s')); first eapply lfilled_es_type_exists; eauto.
     destruct H1 as [lab' [t1s' [t2s' Het]]].
     rewrite upd_label_overwrite in Het.
     by eapply IHHReduce; eauto.
@@ -1741,8 +1759,8 @@ Lemma t_preservation_e: forall s f es s' f' es' C t1s t2s lab ret hs hs',
     store_typing s' ->
     inst_typing s f.(f_inst) C ->
     inst_typing s' f.(f_inst) C ->
-    e_typing s (upd_label (upd_local_return C (tc_local C ++ map typeof f.(f_locs)) ret) lab) es (Tf t1s t2s) ->
-    e_typing s' (upd_label (upd_local_return C (tc_local C ++ map typeof f'.(f_locs)) ret) lab) es' (Tf t1s t2s).
+    e_typing s (upd_label (upd_local_return C (map typeof f.(f_locs) ++ tc_local C) ret) lab) es (Tf t1s t2s) ->
+    e_typing s' (upd_label (upd_local_return C (map typeof f'.(f_locs) ++ tc_local C) ret) lab) es' (Tf t1s t2s).
 Proof.
   move => s f es s' f' es' C t1s t2s lab ret hs hs' HReduce HST1 HST2.
   move: C ret lab t1s t2s.
@@ -1779,19 +1797,19 @@ Proof.
     remove_bools_options. subst.
     apply et_weakening_empty_1.
     assert (HCEmpty: tc_local C = [::]); first by eapply inst_t_context_local_empty; eauto.
-    rewrite HCEmpty. simpl.
+    rewrite HCEmpty cats0. simpl.
     apply ety_local => //.
     eapply mk_s_typing; eauto.
     eapply mk_frame_typing; eauto.
     apply ety_a'; auto_basic => //=.
-    assert (HC2Empty: tc_label C2 = [::]); first by eapply inst_t_context_label_empty; eauto.
-    rewrite HC2Empty in H12.
     apply bet_block. simpl.
-    rewrite HC2Empty.
     rewrite H8.
     rewrite map_cat => //=.
     rewrite n_zeros_typing.
-    by destruct C2.
+    assert (HC2Empty: tc_local C2 = [::]); first by eapply inst_t_context_local_empty; eauto.
+    rewrite HC2Empty cats0.
+    assert (HC2EmptyLab: tc_label C2 = [::]); first by eapply inst_t_context_label_empty; eauto.
+    by rewrite HC2EmptyLab.
   - (* Invoke host *)
     invert_e_typing'.
     eapply Invoke_func_host_typing in H2_comp as [ts [H8 H9]]; eauto. subst.
@@ -1815,7 +1833,7 @@ Proof.
     invert_be_typing.
     apply ety_a'; auto_basic => //=.
     assert (HCEmpty: tc_local C = [::]); first by eapply inst_t_context_local_empty; eauto.
-    rewrite -> HCEmpty in *.
+    rewrite -> HCEmpty, cats0 in *.
     simpl in *.
     apply nth_error_map in H1_getlocal as [v' [HNth Hvt]]. subst.
     apply bet_weakening_empty_1.
@@ -1921,7 +1939,7 @@ Proof.
       * eapply et_const_agnostic; eauto; last by apply v_to_e_const.
       * eapply et_composition'; eauto.
         { assert (HCEmpty: tc_local C = [::]); first by eapply inst_t_context_local_empty; eauto.
-          rewrite HCEmpty in H2_comp0. rewrite HCEmpty.
+          rewrite -> HCEmpty in H1_comp.
           replace (map typeof f'.(f_locs)) with (map typeof f.(f_locs)); last by eapply t_preservation_vs_type; eauto.
           eapply store_extension_e_typing; try apply HST1 => //; try by [].
           eapply store_extension_reduce; eauto.
diff --git a/theories/type_progress.v b/theories/type_progress.v
index 3d10ac79..42375403 100644
--- a/theories/type_progress.v
+++ b/theories/type_progress.v
@@ -1082,7 +1082,7 @@ Proof.
     { (* Context *)
       assert (E : tc_local C1 = [::]).
       { by eapply inst_t_context_local_empty; eauto. }
-      rewrite E. simpl.
+      rewrite E cats0. simpl.
       by fold_upd_context. }
     { by instantiate (1 := [::]). }
     + unfold terminal_form in H0. destruct H0.
@@ -1114,7 +1114,7 @@ Proof.
     fold_upd_context.
     assert (E' : tc_label (upd_local_return C1 (map typeof f.(f_locs)) None) = [::]).
     { simpl. by eapply inst_t_context_label_empty; eauto. }
-    rewrite -E'.
+    rewrite -E' cats0.
     by destruct C1.
   - by eapply s_typing_lf_br; eauto.
   - by eapply s_typing_lf_return; eauto.
diff --git a/theories/typing.v b/theories/typing.v
index aa64ed42..431f8d59 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -241,23 +241,22 @@ Definition global_agree (g : global) (tg : global_type) : bool :=
 Definition globals_agree (gs : seq global) (n : nat) (tg : global_type) : bool :=
   (n < length gs) && (option_map (fun g => global_agree g tg) (List.nth_error gs n) == Some true).
 
-Definition mem_typing (m : memory) (m_t : memory_type) : bool :=
-  (N.leb m_t.(lim_min) (mem_size m)) &&
-  (m.(mem_max_opt) == m_t.(lim_max)) (* TODO: mismatch *).
-
-Definition memi_agree (ms : list memory) (n : nat) (mem_t : memory_type) : bool :=
-  (n < length ms) &&
-  match List.nth_error ms n with
-  | Some mem => mem_typing mem mem_t
-  | None => false
-  end.
-
 Definition functions_agree (fs : seq function_closure) (n : nat) (f : function_type) : bool :=
   (n < length fs) && (option_map cl_type (List.nth_error fs n) == Some f).
 
+Definition limit_match (l1 l2: limits) : bool :=
+  (N.leb l2.(lim_min) l1.(lim_min)) &&
+    match l2.(lim_max) with
+    | None => true
+    | Some lmax2 =>
+        match l1.(lim_max) with
+        | Some lmax1 => (N.leb lmax1 lmax2)
+        | None => false
+        end
+    end.
+
 Definition tab_typing (t : tableinst) (tt : table_type) : bool :=
-  (tt.(tt_limits).(lim_min) <= tab_size t) &&
-  (t.(table_max_opt) <= tt.(tt_limits).(lim_max)).
+  limit_match (Build_limits (N.of_nat (tab_size t)) t.(table_max_opt)) tt.(tt_limits).
 
 Definition tabi_agree ts (n : nat) (tab_t : table_type) : bool :=
   (n < List.length ts) &&
@@ -266,6 +265,17 @@ Definition tabi_agree ts (n : nat) (tab_t : table_type) : bool :=
   | Some x => tab_typing x tab_t
   end.
 
+Definition mem_typing (m : memory) (m_t : memory_type) : bool :=
+  limit_match (Build_limits (mem_size m) m.(mem_max_opt)) m_t.
+
+Definition memi_agree (ms : list memory) (n : nat) (mem_t : memory_type) : bool :=
+  (n < length ms) &&
+  match List.nth_error ms n with
+  | Some mem => mem_typing mem mem_t
+  | None => false
+  end.
+
+
 Definition inst_typing (s : store_record) (inst : instance) (C : t_context) : bool :=
   let '{| inst_types := ts; inst_funcs := fs; inst_tab := tbs; inst_memory := ms; inst_globs := gs; |} := inst in
   match C with
@@ -283,7 +293,7 @@ Inductive frame_typing: store_record -> frame -> t_context -> Prop :=
     inst_typing s i C ->
     f.(f_inst) = i ->
     map typeof f.(f_locs) = tvs ->
-    frame_typing s f (upd_local C (tc_local C ++ tvs))
+    frame_typing s f (upd_local C (tvs ++ tc_local C))
   .
 
 Lemma functions_agree_injective: forall s i t t',
@@ -305,7 +315,7 @@ Inductive cl_typing : store_record -> function_closure -> function_type -> Prop
   | cl_typing_native : forall i s C C' ts t1s t2s es tf,
     inst_typing s i C ->
     tf = Tf t1s t2s ->
-    C' = upd_local_label_return C (tc_local C ++ t1s ++ ts) ([::t2s] ++ tc_label C) (Some t2s) ->
+    C' = upd_local_label_return C (t1s ++ ts) ([::t2s]) (Some t2s) ->
     be_typing C' es (Tf [::] t2s) ->
     cl_typing s (FC_func_native i tf ts es) (Tf t1s t2s)
   | cl_typing_host : forall s tf h,
diff --git a/theories/typing_inversion.v b/theories/typing_inversion.v
index c16c30ac..d968b662 100644
--- a/theories/typing_inversion.v
+++ b/theories/typing_inversion.v
@@ -934,7 +934,7 @@ Lemma Invoke_func_native_typing: forall s i C a cl tn tm ts es t1s t2s,
     cl = FC_func_native i (Tf tn tm) ts es ->
     exists ts' C', t1s = ts' ++ tn /\ t2s = ts' ++ tm /\
                 inst_typing s i C' /\
-               be_typing (upd_local_label_return C' (tc_local C' ++ tn ++ ts) ([::tm] ++ tc_label C') (Some tm)) es (Tf [::] tm).
+               be_typing (upd_local_label_return C' (tn ++ ts) ([::tm]) (Some tm)) es (Tf [::] tm).
 Proof.
   move => s i C a cl tn tm ts es t1s t2s HType HNth Hcl.
   gen_ind_subst HType => //.