diff --git a/spectec/metatheory/Makefile b/spectec/metatheory/Makefile
new file mode 100644
index 0000000000..bc7a5adf4b
--- /dev/null
+++ b/spectec/metatheory/Makefile
@@ -0,0 +1,5 @@
+default:
+	opam install .
+
+clean:
+	dune clean
\ No newline at end of file
diff --git a/spectec/metatheory/dune-project b/spectec/metatheory/dune-project
new file mode 100644
index 0000000000..97a3db3c01
--- /dev/null
+++ b/spectec/metatheory/dune-project
@@ -0,0 +1,12 @@
+(lang dune 3.11)
+(using coq 0.8)
+(generate_opam_files true)
+
+(package
+  (name metatheory)
+  (synopsis "Spectec Wasm formalisation in Rocq")
+  (depends
+    (coq (>= 9.0))
+    (coq-mathcomp-ssreflect (and (>= 2.0.0) (<= 2.4.0)))
+  )
+)
\ No newline at end of file
diff --git a/spectec/metatheory/metatheory.opam b/spectec/metatheory/metatheory.opam
new file mode 100644
index 0000000000..57f04b41df
--- /dev/null
+++ b/spectec/metatheory/metatheory.opam
@@ -0,0 +1,23 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Spectec Wasm formalisation in Rocq"
+depends: [
+  "dune" {>= "3.11"}
+  "coq" {>= "9.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0.0" & <= "2.4.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
diff --git a/spectec/metatheory/theories/dune b/spectec/metatheory/theories/dune
new file mode 100644
index 0000000000..7ef1f0c5d3
--- /dev/null
+++ b/spectec/metatheory/theories/dune
@@ -0,0 +1,7 @@
+(coq.theory
+  (name MetaSpectec)
+  (theories Stdlib mathcomp HB elpi elpi_elpi)
+  (package metatheory)
+  (flags -w -notation-overridden -w -abstract-large-number -w -ambiguous-paths
+         -w -unused-pattern-matching-variable -w -non-recursive
+         ))
\ No newline at end of file
diff --git a/spectec/metatheory/theories/env.v b/spectec/metatheory/theories/env.v
new file mode 100644
index 0000000000..3e436c9165
--- /dev/null
+++ b/spectec/metatheory/theories/env.v
@@ -0,0 +1,107 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+Require Import Stdlib.FSets.FMapAVL.
+Require Import Stdlib.Structures.OrderedTypeEx.
+From MetaSpectec Require Import syntax.
+Import ListNotations.
+
+Declare Scope env_scope.
+Module StringMap := FMapAVL.Make(String_as_OT).
+
+Definition union {A}
+  (m1 m2 : StringMap.t A) : StringMap.t A :=
+  StringMap.fold (fun k v => StringMap.add k v) m1 m2.
+
+Definition singleton {A} (k : string) (v : A) : StringMap.t A :=
+  StringMap.add k v (StringMap.empty A).
+
+(* TYPING *)
+
+Definition var_def : Type := il_typ.
+Definition typ_def : Type := list il_param * list il_inst.
+Definition rel_def : Type := list il_param * il_typ * list il_rule.
+Definition definition_def : Type := list il_param * il_typ * list il_clause.
+
+(* Typing context *)
+
+Record il_env := {
+  VARS : StringMap.t var_def;
+  TYPS : StringMap.t typ_def;
+  DEFS : StringMap.t definition_def;
+  RELS : StringMap.t rel_def
+}.
+
+Definition empty_vars : StringMap.t var_def := StringMap.empty var_def.
+Definition empty_typs : StringMap.t typ_def := StringMap.empty typ_def.
+Definition empty_defs : StringMap.t definition_def := StringMap.empty definition_def.
+Definition empty_rels : StringMap.t rel_def := StringMap.empty rel_def.
+
+Definition env_empty : il_env := {| VARS := empty_vars; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
+
+Definition append_env (e1 e2 : il_env) : il_env :=
+{|
+  VARS := union e1.(VARS) e2.(VARS);
+  TYPS := union e1.(TYPS) e2.(TYPS);
+  DEFS := union e1.(DEFS) e2.(DEFS);
+  RELS := union e1.(RELS) e2.(RELS) 
+|}.
+
+Definition single_var (x : il_id) (t : il_typ) : il_env :=
+  {| VARS := singleton x t; TYPS := empty_typs; DEFS := empty_defs; RELS := empty_rels |}.
+
+Fixpoint many_vars (xs : list (il_id * il_typ)) : il_env :=
+  match xs with
+  | [] => env_empty
+  | (x, t) :: xs' => append_env (single_var x t) (many_vars xs')
+  end
+.  
+
+Definition single_envtyp (x : il_id) (ps : list il_param) (insts : list il_inst) : il_env :=
+  {| VARS := empty_vars; TYPS := singleton x (ps, insts); DEFS := empty_defs; RELS := empty_rels |}.
+
+Definition single_def (x : il_id) (ps : list il_param) (rt : il_typ) (clauses : list il_clause) : il_env :=
+  {| VARS := empty_vars; TYPS := empty_typs; DEFS := singleton x (ps, rt, clauses); RELS := empty_rels |}.
+
+Definition single_rel (x : il_id) (ps : list il_param) (t : il_typ) (rules : list il_rule) : il_env :=
+  {| VARS := empty_vars; TYPS := empty_typs; DEFS := empty_defs; RELS := singleton x (ps, t, rules) |}.
+
+Notation "x [ i ]v = t" := (StringMap.find i (VARS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]t = t" := (StringMap.find i (TYPS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]d = t" := (StringMap.find i (DEFS x) = Some t) (at level 20) : env_scope.
+Notation "x [ i ]r = t" := (StringMap.find i (RELS x) = Some t) (at level 20) : env_scope.
+Notation "x @@ y" := (append_env x y) (at level 20) : env_scope.
+
+Record store := {
+  S_TYPS : StringMap.t typ_def;
+  S_DEFS : StringMap.t definition_def;
+  S_RELS : StringMap.t rel_def
+}.
+
+Definition store_to_env (s : store) : il_env :=
+  {| VARS := empty_vars; TYPS := s.(S_TYPS); DEFS := s.(S_DEFS); RELS := s.(S_RELS) |}.
+
+Definition env_to_store (e : il_env) : store :=
+  {| S_TYPS := e.(TYPS); S_DEFS := e.(DEFS); S_RELS := e.(RELS) |}.
+
+Fixpoint composeenvs (envs : list il_env) : il_env :=
+  match envs with
+  | [] => env_empty
+  | e1 :: es => append_env e1 (composeenvs es)
+  end
+.
+
+Definition tupenv (t : il_typ) : il_env :=
+  match t with
+  | TupT tups => composeenvs (List.map (fun '(x, t) => single_var x t) tups)
+  | _ => env_empty
+  end
+.
+
+Fixpoint paramenv (ps : list il_param) : il_env :=
+  match ps with
+  | [] => env_empty
+  | ExpP x t :: ps' => append_env (single_var x t) (paramenv ps')
+  | TypP x :: ps' => append_env (single_envtyp x [] []) (paramenv ps')
+  | DefP x ps' rt :: ps'' => append_env (single_def x ps' rt []) (paramenv ps'')
+  end
+. 
\ No newline at end of file
diff --git a/spectec/metatheory/theories/numerics.v b/spectec/metatheory/theories/numerics.v
new file mode 100644
index 0000000000..bf88a513a2
--- /dev/null
+++ b/spectec/metatheory/theories/numerics.v
@@ -0,0 +1,166 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import all_ssreflect all_algebra ssrnat ssrint.
+Import GRing.Theory.
+From MetaSpectec Require Import syntax.
+
+Coercion absz : int >-> nat.
+
+Coercion ratz: int >-> rat.
+
+(* Booleans *)
+
+Definition boolun (op : boolunop) (b : bool) : bool :=
+  match op with
+  | NotOp => negb b
+  end
+.
+
+Definition boolbin (op : boolbinop) (b1 b2 : bool) : bool :=
+  match op with
+  | AndOp => b1 && b2
+  | OrOp => b1 || b2
+  | ImplOp => b1 ==> b2
+  | EquivOp => b1 ==> b2 && b2 ==> b1
+  end
+.
+
+Definition iszero (x : il_num) : bool := 
+  match x with
+  | NatE n => n == 0%nat
+  | IntE i => i == 0%R
+  | RatE r => r == 0%R
+  | RealE r => r == 0%R
+  end
+.
+
+Definition isone (x : il_num) : bool := 
+  match x with
+  | NatE n => n == 1%nat
+  | IntE i => i == 1%R
+  | RatE r => r == 1%R 
+  | RealE r => r == 1%R
+  end
+.
+
+Definition isneg (x : il_num) : bool :=
+  match x with
+  | NatE n => false
+  | IntE i => (i < 0)%R
+  | RatE r => (r < 0)%R 
+  | RealE r => (r < 0)%R
+  end
+.
+
+Definition option_map {α β : Type} (f : α -> β) (x : option α) : option β :=
+	match x with
+  | Some x => Some (f x)
+  | _ => None
+	end.
+
+Definition option_join {α : Type} (x : option (option α)) : option α :=
+  match x with
+  | Some None => None
+  | None => None
+  | Some (Some x') => Some x'
+  end.
+
+(* Numerics *)
+
+Definition rat_to_int (x : rat) : option int :=
+  if isone (IntE (denq x)) then Some (numq x) else None
+.
+
+Definition int_to_nat_num (x : int) : option il_num :=
+  if (x >= 0)%R then Some (NatE x) else None.
+
+Definition to_nat (x : R) : nat :=
+  (Num.floor x).
+
+Definition rat_to_R (q : rat) : R :=
+  ((numq q)%:~R / (denq q)%:~R)%R.
+
+(* TODO finish some of the conversions - especially for reals *)
+Definition numcvt (nt : numtyp) (val : il_num) : option il_num :=
+  match nt, val with
+  | NatT, NatE n => Some (NatE n)
+  | NatT, IntE i => int_to_nat_num i
+  | NatT, RatE r => let opt := rat_to_int r in
+    option_join (option_map (fun i => int_to_nat_num i) opt)
+  | NatT, RealE r => Some (NatE (to_nat r))
+  | IntT, NatE n => Some (IntE n)
+  | IntT, IntE i => Some (IntE i)
+  | IntT, RatE r => if isone (IntE (denq r)) then Some (IntE (numq r)) else None
+  | IntT, RealE r => Some (IntE (Num.floor r))
+  | RatT, NatE n => Some (RatE (n%:Q))
+  | RatT, IntE i => Some (RatE (i%:Q))
+  | RatT, RatE r => Some (RatE r)
+  (* TODO think of a better way to cvt real to rational *)
+  | RatT, RealE r => Some (RatE (Num.floor r)%:Q)
+  | RealT, NatE n => Some (RealE (n%:R))
+  | RealT, IntE i => Some (RealE (i%:R))
+  | RealT, RatE r => Some (RealE (rat_to_R r))
+  | RealT, RealE r => Some (RealE r)
+  end
+.
+
+Definition numun (op : numunop) (val : il_num) : option il_num :=
+  match op, val with
+  | PlusOp, n => Some n
+  | MinusOp, NatE n => Some (IntE (0 - n%:R)%R) 
+  | MinusOp, IntE i => Some (IntE (0 - i)%R)
+  | MinusOp, RatE r => Some (RatE (0 - r)%R)
+  | MinusOp, RealE r => Some (RealE (0 - r)%R)
+  end
+.
+
+Definition numbin (op : numbinop) (val1 val2 : il_num) : option il_num :=
+  match op, val1, val2 with
+  | AddOp, NatE n1, NatE n2 => Some (NatE (n1 + n2)%nat)
+  | AddOp, IntE i1, IntE i2 => Some (IntE (i1 + i2)%R)
+  | AddOp, RatE r1, RatE r2 => Some (RatE (r1 + r2)%R)
+  | AddOp, RealE r1, RealE r2 => Some (RealE (r1 + r2)%R)
+  | SubOp, NatE n1, NatE n2 => if (n1 >= n2)%nat then Some (NatE (n1 - n2)%nat) else None
+  | SubOp, IntE i1, IntE i2 => Some (IntE (i1 - i2)%R)
+  | SubOp, RatE r1, RatE r2 => Some (RatE (r1 - r2)%R)
+  | SubOp, RealE r1, RealE r2 => Some (RealE (r1 - r2)%R)
+  | MulOp, NatE n1, NatE n2 => Some (NatE (n1 * n2)%nat)
+  | MulOp, IntE i1, IntE i2 => Some (IntE (i1 * i2)%R)
+  | MulOp, RatE r1, RatE r2 => Some (RatE (r1 * r2)%R)
+  | MulOp, RealE r1, RealE r2 => Some (RealE (r1 * r2)%R)
+  | DivOp, NatE n1, NatE n2 => if negb (iszero val2) then Some (NatE (Nat.div n1 n2)) else None
+  | DivOp, IntE i1, IntE i2 => if negb (iszero val2) then Some (IntE (divz i1 i2)) else None
+  | DivOp, RatE r1, RatE r2 => if negb (iszero val2) then Some (RatE (r1 / r2)%R) else None
+  | DivOp, RealE r1, RealE r2 => if negb (iszero val2) then Some (RealE (r1 / r2)%R) else None
+  | ModOp, NatE n1, NatE n2 => if negb (iszero val2) then Some (NatE (Nat.modulo n1 n2)) else None
+  | ModOp, IntE i1, IntE i2 => if negb (iszero val2) then Some (NatE (modz i1 i2)) else None
+  | PowOp, NatE n1, NatE n2 => Some (NatE (n1^n2))
+  | PowOp, IntE i1, IntE i2 => if (i2 >= 0)%R then Some (IntE (i1^i2)) else None 
+  | PowOp, RatE r1, RatE r2 => if isone (IntE (denq r2)) then Some (RatE (r1^(numq r2))) else None 
+  (* TODO - don't know how this is supposed to work: 
+  | PowOp, RealE r1, RealE r2 => RealE (r1^r2) *)
+  | _, _, _ => None
+  end
+.
+
+
+Definition numcmp (op : numcmpop) (val1 val2 : il_num) : option bool :=
+  match op, val1, val2 with
+  | LtOp, NatE n1, NatE n2 => Some ((n1 < n2)%nat)
+  | LtOp, IntE i1, IntE i2 => Some ((i1 < i2)%R)
+  | LtOp, RatE r1, RatE r2 => Some ((r1 < r2)%R)
+  | LtOp, RealE r1, RealE r2 => Some ((r1 < r2)%R)
+  | GtOp, NatE n1, NatE n2 => Some ((n1 > n2)%nat)
+  | GtOp, IntE i1, IntE i2 => Some ((i1 > i2)%R)
+  | GtOp, RatE r1, RatE r2 => Some ((r1 > r2)%R)
+  | GtOp, RealE r1, RealE r2 => Some ((r1 > r2)%R)
+  | LeOp, NatE n1, NatE n2 => Some ((n1 <= n2)%nat)
+  | LeOp, IntE i1, IntE i2 => Some ((i1 <= i2)%R)
+  | LeOp, RatE r1, RatE r2 => Some ((r1 <= r2)%R)
+  | LeOp, RealE r1, RealE r2 => Some ((r1 <= r2)%R)
+  | GeOp, NatE n1, NatE n2 => Some ((n1 >= n2)%nat)
+  | GeOp, IntE i1, IntE i2 => Some ((i1 >= i2)%R)
+  | GeOp, RatE r1, RatE r2 => Some ((r1 >= r2)%R)
+  | GeOp, RealE r1, RealE r2 => Some ((r1 >= r2)%R)
+  | _, _, _ => None
+  end
+.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/reduction.v b/spectec/metatheory/theories/reduction.v
new file mode 100644
index 0000000000..3db73b318a
--- /dev/null
+++ b/spectec/metatheory/theories/reduction.v
@@ -0,0 +1,792 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+From MetaSpectec Require Import syntax subst env numerics utils.
+Import ListNotations.
+Open Scope env_scope.
+
+Inductive match_args : store -> list il_arg -> list il_quant -> list il_arg -> il_subst -> Prop :=
+  | ma_rule : forall s ags qs ags' sbst,
+    ags = List.map (subst_arg sbst) ags' ->
+    match_args s ags qs ags' sbst
+.
+
+Inductive step_exp: store -> il_exp -> il_exp -> Prop :=
+  (* UnE Rules *)
+  | se_unop_ctx : forall s op e1 e2,
+    step_exp s e1 e2 ->
+    step_exp s (UnE op e1) (UnE op e2)
+  | se_unop_bool : forall s boolop b,
+    step_exp s (UnE (BoolUnop boolop) (BoolE b)) (BoolE (boolun boolop b))
+  | se_unop_num : forall s numop n n',
+    (numun numop n) = Some n' ->
+    step_exp s (UnE (NumUnop numop) (NumE n)) (NumE n')
+
+  (* BinE Rules *)
+  | se_bin_ctxl : forall s op e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_exp s (BinE op e1 e2) (BinE op e1' e2)
+  | se_bin_ctxr : forall s op e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (BinE op e1 e2) (BinE op e1 e2')
+  | se_bin_bool : forall s boolop b1 b2,
+    step_exp s (BinE (BoolBinop boolop) (BoolE b1) (BoolE b2)) (BoolE (boolbin boolop b1 b2))
+  | se_bin_num : forall s numop n1 n2 n3,
+    (numbin numop n1 n2) = Some n3 ->
+    step_exp s (BinE (NumBinop numop) (NumE n1) (NumE n2)) (NumE n3)
+
+  (* CmpE Rules *)
+  | se_cmp_ctxl : forall s op e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_exp s (CmpE op e1 e2) (CmpE op e1' e2)
+  | se_cmp_ctxr : forall s op e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (CmpE op e1 e2) (CmpE op e1 e2')
+  | se_cmp_eq_true : forall s v1 v2,
+    v1 = v2 ->
+    step_exp s (CmpE (BoolCmpop EqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE true)
+  | se_cmp_eq_false : forall s v1 v2,
+    v1 <> v2 ->
+    step_exp s (CmpE (BoolCmpop EqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE false)
+  | se_cmp_ne_false : forall s v1 v2,
+    v1 = v2 ->
+    step_exp s (CmpE (BoolCmpop NeqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE false)
+  | se_cmp_ne_true : forall s v1 v2,
+    v1 <> v2 ->
+    step_exp s (CmpE (BoolCmpop NeqOp) (val_to_exp v1) (val_to_exp v2)) (BoolE true)
+  | se_cmp_num : forall s numcmpop n1 n2 b,
+    (numcmp numcmpop n1 n2) = Some b ->
+    step_exp s (CmpE (NumCmpop numcmpop) (NumE n1) (NumE n2)) (BoolE b)
+  | se_cmp_opt_ctx : forall s opt_e e e',
+    opt_e = Some e ->
+    step_exp s e e' ->
+    step_exp s (OptE opt_e) (OptE (Some e'))
+
+  (* ListE rules *)
+  | se_list_ctx : forall s es es',
+    List.Forall2 (fun e e' => step_exp s e e') es es' ->
+    step_exp s (ListE es) (ListE es')
+
+  (* TupE rules *)
+  | se_tup_ctx : forall s es es',
+    List.Forall2 (fun e e' => step_exp s e e') es es' ->
+    step_exp s (TupE es) (TupE es')
+
+  (* StrE rules *)
+  | se_str_ctx : forall s fields fields',
+    List.Forall2 (fun f f' => step_exp s (snd f) (snd f')) fields fields' ->
+    step_exp s (StrE fields) (StrE fields')
+
+  (* CaseE rules *)
+  | se_case_ctx : forall s m e e',
+    step_exp s e e' ->
+    step_exp s (CaseE m e) (CaseE m e')
+
+  (* LiftE rules *)
+  | se_lift_ctx : forall s e e',
+    step_exp s e e' ->
+    step_exp s (LiftE e) (LiftE e')
+  | se_lift_none : forall s, step_exp s (LiftE (OptE None)) (ListE [])
+  | se_lift_some : forall s e , step_exp s (LiftE (OptE (Some e))) (ListE [e])
+
+  (* ProjE rules *)
+  | se_proj_ctx : forall s e e' n,
+    step_exp s e e' ->
+    step_exp s (ProjE e n) (ProjE e' n)
+  | se_proj_tup : forall s es e_n n,
+    List.nth_error es n = Some e_n ->
+    step_exp s (ProjE (TupE es) n) e_n 
+
+  (* LenE rules *)
+  | se_len_ctx : forall s e e',
+    step_exp s e e' ->
+    step_exp s (LenE e) (LenE e')
+  | se_len_list : forall s es,
+    step_exp s (LenE (ListE es)) (NumE (NatE (List.length es)))
+
+  (* MemE rules *)
+  | se_mem_ctxl : forall s e1 e2 e1',
+    step_exp s e1 e1' ->
+    step_exp s (MemE e1 e2) (MemE e1' e2)
+  | se_mem_ctxr : forall s e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (MemE e1 e2) (MemE e1 e2')
+  | se_mem_true : forall s v1 v2s,
+    List.In v1 v2s ->
+    step_exp s (MemE (val_to_exp v1) (ListE (List.map val_to_exp v2s))) (BoolE true)
+  | se_mem_false : forall s v1 v2s,
+    List.Forall (fun v2 => v1 <> v2) v2s ->
+    step_exp s (MemE (val_to_exp v1) (ListE (List.map val_to_exp v2s))) (BoolE false)
+
+  (* CatE rules *)
+  | se_cat_ctxl : forall s e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_exp s (CatE e1 e2) (CatE e1' e2)
+  | se_cat_ctxr : forall s e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (CatE e1 e2) (CatE e1 e2')
+  | se_cat_opt1 : forall s e1,
+    step_exp s (CatE (OptE (Some e1)) (OptE None)) (OptE (Some e1))
+  | se_cat_opt2 : forall s e2,
+    step_exp s (CatE (OptE None) (OptE (Some e2))) (OptE (Some e2))
+  | se_cat_list : forall s es1 es2,
+    step_exp s (CatE (ListE es1) (ListE es2)) (ListE (es1 ++ es2))
+  | se_cat_str : forall s fields1 fields2,
+    List.Forall2 (fun '(a, _) '(a', _) => a = a') fields1 fields2 ->
+    step_exp s (CatE (StrE fields1) (StrE fields2)) (StrE (list_zipWith (fun x y => (fst x, CatE (snd x) (snd y))) fields1 fields2))
+  
+  (* AccE rules *)
+  | se_acc_ctxexp : forall s e e' p,
+    step_exp s e e' ->
+    step_exp s (AccE e p) (AccE e' p)
+  | se_acc_ctxpath : forall s e p p',
+    step_path s p p' ->
+    step_exp s (AccE e p) (AccE e p')
+  | se_acc_root : forall s e,
+    step_exp s (AccE e RootP) e
+  | se_acc_the : forall s e e' p,
+    step_exp s (AccE e p) (OptE (Some e')) ->
+    step_exp s (AccE e (TheP p)) e'
+  | se_acc_idx : forall s e e_lst' e_n' p n,
+    step_exp s (AccE e p) (ListE e_lst') ->
+    n < List.length e_lst' ->
+    List.nth_error e_lst' n = Some e_n' ->
+    step_exp s (AccE e (IdxP p (NumE (NatE n)))) e_n'
+  | se_acc_slice : forall s e p n m e'_lst e''_lst,
+    step_exp s (AccE e p) (ListE e'_lst) ->
+    n <= m ->
+    n < List.length e'_lst /\ (n + m) < List.length e'_lst ->
+    e''_lst = slice n m e'_lst ->
+    step_exp s (AccE e (SliceP p (NumE (NatE n)) (NumE (NatE n)))) (ListE e''_lst)
+  | se_acc_dot : forall s e p a e_n' fields n,
+    step_exp s (AccE e p) (StrE fields) ->
+    List.nth_error fields n = Some (a, e_n') ->
+    step_exp s (AccE e (DotP p a)) e_n'
+  | se_acc_uncase : forall s e p m e',
+    step_exp s (AccE e p) (CaseE m e') ->
+    step_exp s (AccE e (UncaseP p m)) e'
+
+  (* UpdE rules *)
+  | se_upd_ctxl : forall s e1 e1' p e2,
+    step_exp s e1 e1' ->
+    step_exp s (UpdE e1 p e2) (UpdE e1' p e2)
+  | se_upd_ctxm : forall s e1 p p' e2,
+    step_path s p p' ->
+    step_exp s (UpdE e1 p e2) (UpdE e1 p' e2)
+  | se_upd_ctxr : forall s e1 p e2 e2',
+    step_exp s e2 e2' ->
+    step_exp s (UpdE e1 p e2) (UpdE e1 p e2')
+  | se_upd_root : forall s e1 e2,
+    step_exp s (UpdE e1 RootP e2) e2
+  | se_upd_the : forall s e1 p e2 e',
+    step_exp s (AccE e1 p) (OptE (Some e')) ->
+    step_exp s (UpdE e1 (TheP p) e2) (UpdE e1 p (OptE (Some e2)))
+  | se_upd_idx : forall s e1 p n e2 e_lst',
+    step_exp s (AccE e1 p) (ListE e_lst') ->
+    n < size e_lst' ->
+    step_exp s (UpdE e1 (IdxP p (NumE (NatE n))) e2) (UpdE e1 p (ListE (update e_lst' n e2)))
+  | se_upd_slice : forall s e1 p n m e2_lst e_lst',
+    step_exp s (AccE e1 p) (ListE e_lst') ->
+    n <= m ->
+    n < size e_lst' ->
+    (n + m) < size e_lst' ->
+    step_exp s (UpdE e1 (SliceP p (NumE (NatE n)) (NumE (NatE m))) (ListE e2_lst)) (UpdE e1 p (ListE (update_slice e_lst' n m e2_lst)))
+  | se_upd_dot : forall s e1 p e2 fields a e' n,
+    step_exp s (AccE e1 p) (StrE fields) ->
+    List.nth_error fields n = Some (a, e') ->
+    step_exp s (UpdE e1 (DotP p a) e2) (UpdE e1 p (StrE (update fields n (a, e2))))
+  | se_upd_uncase : forall s e1 p m e2 e', 
+    step_exp s (AccE e1 p) (CaseE m e') ->
+    step_exp s (UpdE e1 (UncaseP p m) e2) (UpdE e1 p (CaseE m e2))
+
+  (* ExtE rule *)
+  | se_ext : forall s e1 p e2,
+    step_exp s (ExtE e1 p e2) (UpdE e1 p (CatE (AccE e1 p) e2))
+
+  (* IterE rules *)
+  | se_iter_ctx1 : forall s e it eps e',
+    step_exp s e e' ->
+    step_exp s (IterE e it eps) (IterE e' it eps)
+  | se_iter_ctx2 : forall s e it it' eps,
+    step_iter s it it' ->
+    step_exp s (IterE e it eps) (IterE e it' eps)
+  | se_iter_ctx3 : forall s e it eps n ep ep',
+    List.nth_error eps n = Some ep ->
+    step_exppull s ep ep' ->
+    step_exp s (IterE e it eps) (IterE e it (update eps n ep'))
+  | se_iter_quest : forall s e xs es,
+    let es' := List.map opt_to_lst es in
+    let es'' := transpose es' in
+    let es''' := lst_to_opt es'' in
+    let ids := List.map fst xs in 
+    same_size es' ->
+    size xs = size es ->
+    size es'' <= 1 ->
+    step_exp s (IterE e I_OPT (list_zipWith (fun x e' => (x, OptE e')) xs es))
+    (OptE (option_map (fun ess => subst_exp (many_svars (zip ids ess)) e) es'''))
+  | se_iter_plus : forall s e xs ess,
+    same_size ess ->
+    seq.all (fun es => size es >= 1) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_exp s (IterE e I_PLUS res_ess) (IterE e I_STAR res_ess)
+  | se_iter_star : forall s e xs ess n y,
+    seq.all (fun es => size es == n) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_exp s (IterE e I_STAR res_ess) (IterE e (I_SUP y (NumE (NatE n))) res_ess)
+  | se_iter_sup : forall s e x_i n xs ess,
+    seq.all (fun es => size es == n) ess ->
+    size xs = size ess -> 
+    let ess' := transpose ess in
+    let ids := List.map fst xs in
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    let res_ess' := (list_mapi (fun i es => 
+      let sbst := subst_svar x_i (NumE (NatE i)) in
+      let sbst' := many_svars (zip ids es) in
+      subst_exp (append_subst sbst sbst') e 
+    ) ess') in
+    step_exp s (IterE e (I_SUP x_i (NumE (NatE n))) res_ess) (ListE res_ess')
+
+  (* CallE rules *)
+  | se_call_ctx : forall s x ags n a a',
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_exp s (CallE x ags) (CallE x (update ags n a'))
+  | se_call_app : forall s x ags cs ps t,
+    StringMap.find x (DEFS (store_to_env s)) = Some (ps, t, cs) ->
+    step_exp s (CallE x ags) (MatchE ags cs)
+
+  (* CvtE rules *)
+  | se_cvt_ctx : forall s e nt1 nt2 e',
+    step_exp s e e' ->
+    step_exp s (CvtE e nt1 nt2) (CvtE e' nt1 nt2)
+  | se_cvt_num : forall s num nt1 nt2 e,
+    numcvt nt2 num = Some e ->
+    step_exp s (CvtE (NumE num) nt1 nt2) (NumE e)
+
+  (* SubE rules *)
+  | se_sub_ctx1 : forall s e t1 t2 e',
+    step_exp s e e' ->
+    step_exp s (SubE e t1 t2) (SubE e' t1 t2)
+  | se_sub_ctx2 : forall s e t1 t1' t2,
+    step_typ s t1 t1' ->
+    step_exp s (SubE e t1 t2) (SubE e t1' t2)
+  | se_sub_ctx3 : forall s e t1 t2 t2',
+    step_typ s t2 t2' ->
+    step_exp s (SubE e t1 t2) (SubE e t1 t2')
+  | se_sub_refl : forall s e t,
+    step_exp s (SubE e t t) e
+  | se_sub_sub : forall s e' t1' t2' t1 t2,
+    step_exp s (SubE (SubE e' t1' t2') t1 t2) (SubE e' t1' t2)
+  | se_sub_tup : forall s es tups tups',
+    size es = size tups ->
+    size tups = size tups' ->
+    let sbst1 := many_svars (list_zipWith (fun e '(x1, _) => (x1, e)) es tups) in
+    let sbst2 := many_svars (list_zipWith (fun e '(x2, _) => (x2, e)) es tups') in
+    step_exp s (SubE (TupE es) (TupT tups) (TupT tups')) 
+    (TupE (List.map (fun '(e, ((_, t1), (_, t2))) => SubE e (subst_typ sbst1 t1) (subst_typ sbst2 t2)) (zip es (zip tups tups'))))
+  | se_sub_opt : forall s e_opt t1 t2,
+    step_exp s (SubE (OptE e_opt) (IterT t1 I_OPT) (IterT t2 I_OPT)) (OptE (option_map (fun e => SubE e t1 t2) e_opt))
+  | se_sub_list : forall s es t1 t2,
+    step_exp s (SubE (ListE es) (IterT t1 I_STAR) (IterT t2 I_STAR)) (ListE (List.map (fun e => SubE e t1 t2) es))
+  | se_sub_case : forall s (e : il_exp) op e x1 x2 t1 t2 t1' t2' tcs1 tcs2 qs1 qs2 prs1 prs2,
+    t1 = MatchT x1 [] [([], [], VariantT tcs1)] ->
+    t2 = MatchT x2 [] [([], [], VariantT tcs2)] ->    
+    List.In (op, qs1, t1', prs1) tcs1 ->
+    List.In (op, qs2, t2', prs2) tcs2 ->
+    step_exp s (SubE (CaseE op e) t1 t2) (CaseE op (SubE e t1' t2'))
+  | se_sub_str : forall s efs x1 x2 t1 t2 t1s t2s tfs1 tfs2 ats es,
+    t1 = MatchT x1 [] [([], [], StructT tfs1)] ->
+    t2 = MatchT x2 [] [([], [], StructT tfs2)] -> 
+    size efs = size tfs1 ->
+    size efs = size tfs2 ->
+    List_Forall3 (fun '(a, t) a' t' => a = a' /\ t = t') (atomtyps tfs2) ats t2s ->
+    List.Forall2 (fun a t => List.In (a, t) (atomtyps tfs1)) ats t1s ->
+    List.Forall2 (fun a e => List.In (a, e) efs) ats es ->
+    step_exp s (SubE (StrE efs) t1 t2)
+    (StrE (list_map3 (fun '(a, e) t1 t2 => (a, SubE e t1 t2)) (zip ats es) t1s t2s)) 
+
+  (* IfE rules *)
+  | se_ife_ctx1 : forall s e1 e2 e3 e1',
+    step_exp s e1 e1' ->
+    step_exp s (IfE e1 e2 e3) (IfE e1' e2 e3)
+  | se_ife_true : forall s e2 e3,
+    step_exp s (IfE (BoolE true) e2 e3) e2
+  | se_ife_false : forall s e2 e3,
+    step_exp s (IfE (BoolE false) e2 e3) e3
+
+  (* MatchE rules *)
+  | se_matche_ctx1 : forall s ags cs a a' n,
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_exp s (MatchE ags cs) (MatchE (update ags n a') cs)
+  | se_matche_ctx2 : forall s ags cs c c' n,
+    List.nth_error cs n = Some c -> 
+    step_clause s c c' ->
+    step_exp s (MatchE ags cs) (MatchE ags (update cs n c'))
+  | se_matche_match : forall s ags qs ags' e prems cs ags'' ags''' qs' sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    let ams' := list_zipWith (fun a a' => MatchA a a') ags'' ags''' in
+    let new_c1 := (qs', ags''', subst_exp sbst e, List.map (subst_prem sbst) prems) in
+    let new_c2 := ([], ags'', MatchE ags (cs), []) in
+    step_argmatch s qs ams sbst qs' ams' ->
+    step_exp s (MatchE ags ((qs, ags', e, prems) :: cs)) (MatchE ags'' [new_c1; new_c2])
+  | se_matche_fail : forall s ags qs ags' e prems cs sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    step_argmatch s qs ams sbst [] [FailA] ->
+    step_exp s (MatchE ags ((qs, ags', e, prems) :: cs)) (MatchE ags cs)
+  | se_matche_guess : forall s ags qs ags' e prems cs sbst,
+    (* TODO ok subst *)
+    (* NOTE: non-computational rule *)
+    step_exp s (MatchE ags ((qs, ags', e, prems) :: cs)) (MatchE ags (([], List.map (subst_arg sbst) ags', e, prems) :: cs))
+  | se_matche_matchtrue : forall s e cs,
+    step_exp s (MatchE [] (([], [], e, []) :: cs)) e
+  | se_matche_matchfalse : forall s e prems cs,
+    step_exp s (MatchE [] (([], [], e, (IfPr (BoolE false)) :: prems) :: cs)) (MatchE [] cs)
+with
+
+step_arg : store -> il_arg -> il_arg -> Prop :=
+  | sa_exp : forall s e e',
+    step_exp s e e' ->
+    step_arg s (ExpA e) (ExpA e')
+  | sa_typ : forall s t t',
+    step_typ s t t' ->
+    step_arg s (TypA t) (TypA t')
+
+with
+
+step_typ : store -> il_typ -> il_typ -> Prop :=
+  | st_var_ctx : forall s x ags n a a',
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_typ s (VarT x ags) (VarT x (update ags n a'))
+  | st_var_app : forall s x ags ps insts,
+    StringMap.find x (TYPS (store_to_env s)) = Some (ps, insts) ->
+    step_typ s (VarT x ags) (MatchT x ags insts)
+  | st_tup_ctx : forall s tups n x t t',
+    List.nth_error tups n = Some (x, t) ->
+    step_typ s t t' ->
+    step_typ s (TupT tups) (TupT (update tups n (x, t')))
+  | st_iter_ctx : forall s t t' it,
+    step_typ s t t' ->
+    step_typ s (IterT t it) (IterT t' it)
+  | st_match_ctx1 : forall s x ags insts n a_n a_n',
+    List.nth_error ags n = Some a_n ->
+    step_arg s a_n a_n' ->
+    step_typ s (MatchT x ags insts) (MatchT x (update ags n a_n') insts)
+  | st_match_ctx2 : forall s x ags insts n inst_n inst_n',
+    List.nth_error insts n = Some inst_n ->
+    step_inst s inst_n inst_n' ->
+    step_typ s (MatchT x ags insts) (MatchT x ags (update insts n inst_n'))
+  | st_match_alias : forall s x t insts,
+    step_typ s (MatchT x [] (([], [], AliasT t) :: insts)) t
+  | st_match_match : forall s x ags ags' ags'' qs qs' ags''' insts dt sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    let ams' := list_zipWith (fun a a' => MatchA a a') ags'' ags''' in
+    let new_dt := AliasT (MatchT x ags insts) in
+    step_argmatch s qs ams sbst qs' ams' ->
+    step_typ s (MatchT x ags ((qs, ags', dt) :: insts)) (MatchT x ags'' [(qs', ags''', subst_deftyp sbst dt); ([], ags'', new_dt)])
+  | st_match_fail : forall s x ags ags' qs insts dt sbst,
+    let ams := list_zipWith (fun a a' => MatchA a a') ags ags' in
+    step_argmatch s qs ams sbst [] [FailA] ->
+    step_typ s (MatchT x ags ((qs, ags', dt) :: insts)) (MatchT x ags insts)
+
+
+with
+
+step_path : store -> il_path -> il_path -> Prop :=
+  | sp_idx_ctxl : forall s p p' e,
+    step_path s p p' ->
+    step_path s (IdxP p e) (IdxP p' e)
+  | sp_idx_ctxr : forall s p e e',
+    step_exp s e e' ->
+    step_path s (IdxP p e) (IdxP p e')
+  | sp_the_ctx : forall s p p',
+    step_path s p p' ->
+    step_path s (TheP p) (TheP p')
+  | sp_uncase_ctx : forall s m p p',
+    step_path s p p' ->
+    step_path s (UncaseP p m) (UncaseP p' m)
+  | sp_slice_ctx1 : forall s p p' e1 e2,
+    step_path s p p' ->
+    step_path s (SliceP p e1 e2) (SliceP p' e1 e2)
+  | sp_slice_ctx2 : forall s p e1 e1' e2,
+    step_exp s e1 e1' ->
+    step_path s (SliceP p e1 e2) (SliceP p e1' e2)
+  | sp_slice_ctx3 : forall s p e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_path s (SliceP p e1 e2) (SliceP p e1 e2')
+  | sp_dot_ctx : forall s p p' a, 
+    step_path s p p' ->
+    step_path s (DotP p a) (DotP p' a) 
+
+with 
+
+step_prems : store -> list il_prem -> list il_prem -> Prop :=
+  | sp_ctx : forall s p ps p' ps',
+    step_prems s [p] p' ->
+    step_prems s (p :: ps) (p' ++ ps')
+
+  (* IfPr rules *)
+  | sp_if_ctx : forall s e e',
+    step_exp s e e' ->
+    step_prems s [IfPr e] [IfPr e']
+  | sp_if_true : forall s,
+    step_prems s [IfPr (BoolE true)] []
+
+  (* LetPr rules *)
+  | sp_let_ctx : forall s e1 e2 e2',
+    step_exp s e2 e2' ->
+    step_prems s [LetPr e1 e2] [LetPr e1 e2']
+  | sp_let : forall s e1 e2 e1' e2',
+    reduce_exp s e1 e1' ->
+    reduce_exp s e2 e2' ->
+    e1' = e2' ->
+    step_prems s [LetPr e1 e2] []
+
+  (* IterPr rules *)
+  | sp_iter_ctx1 : forall s p it eps p',
+    step_prems s [p] [p'] ->
+    step_prems s [IterPr p it eps] [IterPr p' it eps]
+  | sp_iter_ctx2 : forall s p it it' eps p',
+    step_iter s it it' ->
+    step_prems s [IterPr p it eps] [IterPr p' it eps]
+  | sp_iter_ctx3 : forall s pr it eps n ep ep',
+    List.nth_error eps n = Some ep ->
+    step_exppull s ep ep' ->
+    step_prems s [IterPr pr it eps] [IterPr pr it (update eps n ep')]
+  | sp_iter_quest : forall s pr xs es,
+    let es' := List.map opt_to_lst es in
+    let es'' := transpose es' in
+    let es''' := lst_to_opt es'' in
+    let ids := List.map fst xs in 
+    same_size es' ->
+    size xs = size es ->
+    size es'' <= 1 ->
+    step_prems s [IterPr pr I_OPT (list_zipWith (fun x e' => (x, OptE e')) xs es)]
+    (opt_to_lst (option_map (fun ess => subst_prem (many_svars (zip ids ess)) pr) es'''))
+  | sp_iter_plus : forall s pr xs ess,
+    same_size ess ->
+    seq.all (fun es => size es >= 1) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_prems s [IterPr pr I_PLUS res_ess] [IterPr pr I_STAR res_ess]
+  | sp_iter_star : forall s pr xs ess n y,
+    seq.all (fun es => size es == n) ess ->
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    step_prems s [IterPr pr I_STAR res_ess] [IterPr pr (I_SUP y (NumE (NatE n))) res_ess]
+  | sp_iter_sup : forall s pr x_i n xs ess,
+    seq.all (fun es => size es == n) ess ->
+    size xs = size ess -> 
+    let ess' := transpose ess in
+    let res_ess := (list_zipWith (fun x es => (x, ListE es)) xs ess) in
+    let ids := List.map fst xs in 
+    let res_ess' := (list_mapi (fun i es => 
+      let sbst := subst_svar x_i (NumE (NatE i)) in
+      let sbst' := many_svars (zip ids es) in
+      subst_prem (append_subst sbst sbst') pr 
+    ) ess') in
+    step_prems s [IterPr pr (I_SUP x_i (NumE (NatE n))) res_ess] res_ess'
+
+  (* ElsePr rule *)
+  | sp_else : forall s,
+    step_prems s [ElsePr] [IfPr (BoolE true)]
+
+  (* NegPr rules *)
+  | sp_neg_ctx : forall s p p',
+    step_prems s [p] [p'] ->
+    step_prems s [NegPr p] [NegPr p']
+  | sp_neg_bool: forall s b,
+    step_prems s [NegPr (IfPr (BoolE b))] [IfPr (BoolE (negb b))]
+  
+  (* RelPr rule (Non-computational) *)
+  | sp_rel : forall s x ags e sbst prems e' ps t rules qs,
+    StringMap.find x (RELS (store_to_env s)) = Some (ps, t, rules) ->
+    let rules' := List.map (fun r => subst_rule (args_for_params ags ps) r) rules in
+    List.In (qs, e', prems) rules' ->    
+    (* TODO ok_subst *) 
+    step_prems s [RulePr x ags e] (List.map (subst_prem sbst) prems ++ [IfPr (CmpE (BoolCmpop EqOp) (subst_exp sbst e') e)])
+
+with
+
+step_iter : store -> iter -> iter -> Prop :=
+  | si_ctx : forall s x e e',
+    step_exp s e e' ->
+    step_iter s (I_SUP x e) (I_SUP x e')
+
+with
+
+step_exppull : store -> exppull -> exppull -> Prop :=
+  | sep_ctx : forall s x e e',
+    step_exp s e e' ->
+    step_exppull s (x, e) (x, e')
+
+with 
+
+reduce_exp : store -> il_exp -> il_exp -> Prop :=
+  | re_refl : forall s e, reduce_exp s e e
+  | re_step : forall s e1 e2 e3,
+    step_exp s e1 e3 ->
+    reduce_exp s e2 e3 ->
+    reduce_exp s e1 e3
+
+with
+
+reduce_prems : store -> list il_prem -> list il_prem -> Prop :=
+  | rp_refl : forall s p, reduce_prems s p p
+  | rp_step : forall s p1 p2 p3,
+    step_prems s p1 p2 ->
+    reduce_prems s p2 p3 ->
+    reduce_prems s p1 p3
+
+with
+
+step_inst : store -> il_inst -> il_inst -> Prop :=
+  | sti_ctx : forall s qs ags t a a' n,
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_inst s (qs, ags, t) (qs, update ags n a', t)
+
+with
+
+step_clause : store -> il_clause -> il_clause -> Prop :=
+  | stc_ctx1 : forall s qs ags e prems a a' n,
+    List.nth_error ags n = Some a ->
+    step_arg s a a' ->
+    step_clause s (qs, ags, e, prems) (qs, update ags n a', e, prems)
+  | stc_ctx2 : forall s qs ags e prems e',
+    step_exp s e e' ->
+    step_clause s (qs, ags, e, prems) (qs, ags, e', prems)
+  | stc_ctx3 : forall s qs ags e prems prems',
+    step_prems s prems prems' ->
+    step_clause s (qs, ags, e, prems) (qs, ags, e, prems')
+
+with
+
+step_argmatch_plain : store -> list argmatch -> list argmatch -> Prop :=
+  | sagp_ctx1 : forall s a a' a'',
+    step_arg s a a'' ->
+    step_argmatch_plain s [MatchA a a'] [MatchA a'' a']
+  | sagp_ctx2 : forall s a a' a'',
+    step_arg s a' a'' ->
+    step_argmatch_plain s [MatchA a a'] [MatchA a a'']
+  | sagp_eq : forall s a,
+    step_argmatch_plain s [MatchA a a] []
+    (* TODO disjointness *)
+
+with
+
+step_expmatch_plain : store -> list expmatch -> list expmatch -> Prop :=
+  | semp_ctx1 : forall s e e' e'',
+    step_exp s e e'' ->
+    step_expmatch_plain s [MatchEM e e'] [MatchEM e'' e']
+  | semp_ctx2 : forall s e e' e'',
+    step_exp s e' e'' ->
+    step_expmatch_plain s [MatchEM e e'] [MatchEM e e'']
+  | semp_eq : forall s e,
+    step_expmatch_plain s [MatchEM e e] []
+  | semp_unplus : forall s num e,
+    negb (isneg num) ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop PlusOp) e)] [MatchEM (NumE num) e]
+  | semp_unplus_false : forall s num e,
+    isneg num ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop PlusOp) e)] [FailEM]
+  | semp_unminus : forall s num num' e,
+    isneg num ->
+    numun MinusOp num = Some num' ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop MinusOp) e)] [MatchEM (NumE num') e] 
+  | semp_unminus_false : forall s num e,
+    negb (isneg num) ->
+    step_expmatch_plain s [MatchEM (NumE num) (UnE (NumUnop MinusOp) e)] [FailEM]
+  | semp_cvt : forall s num e nt1 nt2 num',
+    numcvt nt1 num = Some num' ->
+    step_expmatch_plain s [MatchEM (NumE num) (CvtE e nt1 nt2)] [MatchEM (NumE num') e]
+  | semp_cvt_false : forall s num e nt1 nt2,
+    numcvt nt1 num = None ->
+    step_expmatch_plain s [MatchEM (NumE num) (CvtE e nt1 nt2)] [FailEM]
+  | semp_tup : forall s tups tups',
+    size tups = size tups' ->
+    step_expmatch_plain s [MatchEM (TupE tups) (TupE tups')] (list_zipWith (fun e e' => MatchEM e e') tups tups')
+  | semp_case : forall s e e' op,
+    step_expmatch_plain s [MatchEM (CaseE op e) (CaseE op e')] [MatchEM e e']
+  | semp_case_fail : forall s e e' op op',
+    op <> op' ->
+    step_expmatch_plain s [MatchEM (CaseE op e) (CaseE op' e')] [MatchEM e e']
+  | semp_opt : forall s e e',
+    same_opt e e' ->
+    step_expmatch_plain s [MatchEM (OptE e) (OptE e')] (list_zipWith (fun e1 e2 => MatchEM e1 e2) (opt_to_lst e) (opt_to_lst e'))
+  | semp_opt_fail : forall s e e',
+    negb (same_opt e e') ->
+    step_expmatch_plain s [MatchEM (OptE e) (OptE e')] [FailEM]
+  | semp_list : forall s es es',
+    size es = size es' ->
+    step_expmatch_plain s [MatchEM (ListE es) (ListE es')] (list_zipWith (fun e1 e2 => MatchEM e1 e2) es es')
+  | semp_list_fail : forall s es es',
+    size es <> size es' ->
+    step_expmatch_plain s [MatchEM (ListE es) (ListE es')] [FailEM]
+  | semp_lift : forall s es e,
+    size es <= 1 ->
+    step_expmatch_plain s [MatchEM (ListE es) (LiftE e)] [MatchEM (OptE (lst_to_opt es)) e]
+  | semp_lift_fail : forall s es e,
+    size es > 1 ->
+    step_expmatch_plain s [MatchEM (ListE es) (LiftE e)] [FailEM]
+  | semp_cat_left : forall s e1s e2s e1s' e2',
+    size e1s = size e1s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE (ListE e1s') e2')] [MatchEM (ListE e1s) (ListE e1s'); MatchEM (ListE e2s) e2']
+  | semp_cat_left_fail : forall s e1s e2s e1s' e2',
+    size e1s <> size e1s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE (ListE e1s') e2')] [FailEM]
+  | semp_cat_right : forall s e1s e2s e1' e2s',
+    size e2s = size e2s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE e1' (ListE e2s'))] [MatchEM (ListE e1s) e1'; MatchEM (ListE e2s) (ListE e2s')]
+  | semp_cat_right_fail : forall s e1s e2s e1' e2s',
+    size e2s <> size e2s' ->
+    step_expmatch_plain s [MatchEM (ListE (e1s ++ e2s)) (CatE e1' (ListE e2s'))] [FailEM] 
+  | semp_str : forall s efs efs' es,
+    List.Forall2 (fun '(l, e) '(l', e') => l = l' /\ List.In (l, e) efs) es efs' ->
+    step_expmatch_plain s [MatchEM (StrE efs) (StrE efs')] (list_zipWith (fun ef ef' => MatchEM (exp_from_field ef) (exp_from_field ef')) es efs')
+  | semp_iter_plus : forall s es e' eps,
+    size es >= 1 ->
+    step_expmatch_plain s [MatchEM (ListE es) (IterE e' I_PLUS eps)] [MatchEM (ListE es) (IterE e' I_STAR eps)]
+  | semp_iter_plus_fail : forall s es e' eps,
+    es = [] ->
+    step_expmatch_plain s [MatchEM (ListE es) (IterE e' I_PLUS eps)] [FailEM]
+  | semp_iter_star : forall s es e' eps y n,
+    size es = n ->
+    step_expmatch_plain s [MatchEM (ListE es) (IterE e' I_PLUS eps)] [MatchEM (ListE es) (IterE e' (I_SUP y (NumE (NatE n))) eps)]
+    (* TODO y fresh *)
+  | semp_sub_sub : forall s e t1 t2 e' t1' t2',
+    sub_typ (store_to_env s) t1 t1' ->
+    step_expmatch_plain s [MatchEM (SubE e t1 t2) (SubE e' t1' t2')] [MatchEM (SubE e t1 t1') e']
+    (* TODO disjointness *)
+  | semp_sub_tup : forall s es e' typs typs',
+    size es = size typs ->
+    size typs = size typs' ->
+    let sbst1 := many_svars (list_mapi (fun i '(e, (x, _)) => (x, ProjE e i)) (zip es typs)) in
+    let sbst2 := many_svars (list_mapi (fun i '(e, (x, _)) => (x, ProjE e i)) (zip es typs')) in
+    let tups := List.map (fun '((_, t1), (_, t2)) => SubE e' (subst_typ sbst1 t1) (subst_typ sbst2 t2)) (zip typs typs') in
+    step_expmatch_plain s [MatchEM (TupE es) (SubE e' (TupT typs) (TupT typs'))] 
+    [MatchEM (TupE tups) e']
+
+with
+
+step_argmatch : store -> list il_quant -> list argmatch -> il_subst -> list il_quant -> list argmatch -> Prop :=
+  | sam_plain : forall s qs ams ams',
+    step_argmatch_plain s ams ams' ->
+    step_argmatch s qs ams subst_empty qs ams'
+  | sam_seq : forall s q1s qs qs' q2s am1s am am2s ams' sbst,
+    step_argmatch s qs [am] sbst qs' ams' ->
+    let new_q2s :=  List.map (subst_quant sbst) q2s in
+    let new_am2s := List.map (subst_argmatch sbst) am2s in
+    step_argmatch s (q1s ++ qs ++ q2s) (am1s ++ [am] ++ am2s) sbst (q1s ++ qs' ++ new_q2s) (am1s ++ ams' ++ new_am2s)
+  | sam_seq_fail : forall s q1s qs q2s am1s am am2s sbst,
+    step_argmatch s qs [am] sbst [] [FailA] ->
+    step_argmatch s (q1s ++ qs ++ q2s) (am1s ++ [am] ++ am2s) sbst [] [FailA]
+  | sam_typ : forall s x t,
+    let sbst := subst_styp x t in
+    step_argmatch s [TypP x] [MatchA (TypA t) (TypA (VarT x []))] sbst [] []
+  | sam_exp : forall s x t e,
+    let sbst := subst_svar x e in
+    step_argmatch s [ExpP x t] [MatchA (ExpA e) (ExpA (VarE x))] sbst [] []
+  | sam_fun : forall s x ps t y,
+    let sbst := subst_sfun x y in
+    step_argmatch s [DefP x ps t] [MatchA (DefA y) (DefA x)] sbst [] []
+  | sam_exp_exp : forall s qs qs' em ems' sbst,
+    step_expmatch s qs [em] sbst qs' ems' ->
+    step_argmatch s qs [to_argmatch em] sbst qs' (List.map to_argmatch ems')
+  | sam_exp_exp_fail : forall s qs em sbst,
+    step_expmatch s qs [em] sbst [] [FailEM] ->
+    step_argmatch s qs [to_argmatch em] sbst [] [FailA]
+
+with
+
+step_expmatch : store -> list il_quant -> list expmatch -> il_subst -> list il_quant -> list expmatch -> Prop :=
+  | sem_plain : forall s qs ems ems',
+    step_expmatch_plain s ems ems' ->
+    step_expmatch s qs ems subst_empty qs ems'
+  | sem_seq : forall s q1s qs qs' q2s em1s em em2s ems' sbst,
+    step_expmatch s qs [em] sbst qs' ems' ->
+    let new_q2s :=  List.map (subst_quant sbst) q2s in
+    let new_em2s := List.map (subst_expmatch sbst) em2s in
+    step_expmatch s (q1s ++ qs ++ q2s) (em1s ++ [em] ++ em2s) sbst (q1s ++ qs' ++ new_q2s) (em1s ++ ems' ++ new_em2s)
+  | sem_seq_fail : forall s q1s qs q2s em1s em em2s sbst,
+    step_expmatch s qs [em] sbst [] [FailEM] ->
+    step_expmatch s (q1s ++ qs ++ q2s) (em1s ++ [em] ++ em2s) sbst [] [FailEM]
+  | sem_iter_sup : forall s qs es e' y e_n eps n (xss : list (list il_id)),
+    size es = n ->
+    seq.all (fun xs => size xs == size es) xss ->
+    let xss' := transpose xss in
+    let qs' := List.concat (List.map (fun xs => list_zipWith (fun '(_, t, _) x => ExpP x t) eps xs) xss) in
+    let ems := list_mapi (fun i '(xs, e) => 
+      let sup_sbst := subst_svar y (NumE (NatE i)) in 
+      let sbst := many_svars (List.map (fun '((x, _, _), x') => (x, VarE x')) (zip eps xs)) in
+      MatchEM e (subst_exp (append_subst sup_sbst sbst) e') 
+    ) (zip xss es) in
+    let num_match := [MatchEM (NumE (NatE n)) e_n] in
+    let list_match := list_zipWith (fun xs' '(_, _, ep) => MatchEM (ListE (List.map VarE xs')) ep) xss' eps in
+    step_expmatch s qs [MatchEM (ListE es) (IterE e' (I_SUP y e_n) eps)] subst_empty (qs' ++ qs) (ems ++ num_match ++ list_match)
+  | sem_iter_opt : forall s qs e e' eps (xss : option (list il_id)),
+    let xss' := transpose_opt xss in
+    let qs' := List.concat (List.map (fun xs => list_zipWith (fun '(_, t, _) x => ExpP x t) eps xs) (opt_to_lst xss)) in
+    let ems := list_zipWith (fun xs e => 
+      let sbst := many_svars (List.map (fun '((x, _, _), x') => (x, VarE x')) (zip eps xs)) in
+      MatchEM e (subst_exp sbst e') 
+    ) (opt_to_lst xss) (opt_to_lst e) in
+    let opt_match := list_zipWith (fun xs' '(_, _, ep) => MatchEM (OptE (option_map VarE xs')) ep) xss' eps in
+    step_expmatch s qs [MatchEM (OptE e) (IterE e' I_OPT eps)] subst_empty (qs' ++ qs) (ems ++ opt_match)
+
+with
+
+sub_typ : il_env -> il_typ -> il_typ -> Prop :=
+  | st_tup : forall env x1 t1 x2 t2 tups tups',
+    let env' := (single_var x1 t1) in
+    let sbst := (subst_svar x2 (VarE x1)) in
+    sub_typ env t1 t2 ->
+    sub_typ (env @@ env') (TupT tups) (subst_typ sbst (TupT tups')) -> 
+    sub_typ env (TupT ((x1, t1) :: tups)) (TupT ((x2, t2) :: tups'))
+  | st_struct : forall env t1 t2 tfs1 tfs2,
+    expand_typ (env_to_store env) t1 (StructT tfs1) ->
+    expand_typ (env_to_store env) t2 (StructT tfs2) -> 
+    sub_typ env t1 t2
+  | st_iter : forall env t1 t2 it,
+    sub_typ env t1 t2 ->
+    sub_typ env (IterT t1 it) (IterT t2 it) 
+  | st_refl : forall env t, sub_typ env t t
+  | st_trans : forall env t1 t2 t',
+    sub_typ env t1 t' ->
+    sub_typ env t' t2 ->
+    sub_typ env t1 t2
+
+with
+
+expand_typ : store -> il_typ -> il_deftyp -> Prop :=
+  | et_plain : forall s t t',
+    is_plaintyp t ->
+    reduce_typ s t t' ->
+    expand_typ s t (AliasT t)
+  | et_def : forall s t dt x insts,
+    reduce_typ s t (MatchT x [] (([], [], dt) :: insts)) -> 
+    expand_typ s t dt
+
+with
+
+reduce_typ : store -> il_typ -> il_typ -> Prop :=
+  | rt_refl : forall s t, reduce_typ s t t
+  | rt_step : forall s t1 t2 t3,
+    step_typ s t1 t2 ->
+    reduce_typ s t2 t3 ->
+    reduce_typ s t1 t3
+.
+
+Inductive reduce_arg : store -> il_arg -> il_arg -> Prop :=
+  | ra_refl : forall s a, reduce_arg s a a
+  | ra_step : forall s a1 a2 a3,
+    step_arg s a1 a2 ->
+    reduce_arg s a2 a3 ->
+    reduce_arg s a1 a3
+.
+
+Inductive eq_typ : store -> il_typ -> il_typ -> Prop :=
+  | eq_typ_rule : forall s t1 t2 t1' t2',
+    reduce_typ s t1 t1' ->
+    reduce_typ s t2 t2' ->
+    t1' = t2' ->
+    eq_typ s t1 t2
+.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/subst.v b/spectec/metatheory/theories/subst.v
new file mode 100644
index 0000000000..38d703a476
--- /dev/null
+++ b/spectec/metatheory/theories/subst.v
@@ -0,0 +1,282 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+From MetaSpectec Require Import syntax env.
+Require Import Stdlib.FSets.FMapAVL.
+Require Import Stdlib.Structures.OrderedTypeEx.
+Import ListNotations.
+
+Record il_subst : Type := 
+  {
+  S_EXP : StringMap.t il_exp;
+  S_TYP : StringMap.t il_typ;
+  S_FUN : StringMap.t il_id;
+  }
+.
+
+Definition empty_exp : StringMap.t il_exp := StringMap.empty il_exp.
+Definition empty_typ : StringMap.t il_typ := StringMap.empty il_typ.
+Definition empty_id : StringMap.t il_id := StringMap.empty il_id.
+Definition subst_empty : il_subst := {| S_EXP := empty_exp; S_TYP := empty_typ; S_FUN := empty_id |}.
+
+Definition append_subst (s1 s2 : il_subst) : il_subst :=
+  {|
+  S_EXP := union s1.(S_EXP) s2.(S_EXP);
+  S_TYP := union s1.(S_TYP) s2.(S_TYP);
+  S_FUN := union s1.(S_FUN) s2.(S_FUN) 
+  |}.
+
+Definition subst_svar (x : il_id) (e : il_exp) : il_subst :=
+  {|
+  S_EXP := singleton x e;
+  S_TYP := empty_typ;
+  S_FUN := empty_id
+  |}.
+
+Definition subst_styp (x : il_id) (t : il_typ) : il_subst :=
+  {|
+  S_EXP := empty_exp;
+  S_TYP := singleton x t;
+  S_FUN := empty_id
+  |}.
+
+Definition subst_sfun (x : il_id) (y : il_id) : il_subst :=
+  {|
+  S_EXP := empty_exp;
+  S_TYP := empty_typ;
+  S_FUN := singleton x y
+  |}.
+
+Record dom : Type :=
+  {
+  D_EXP : list il_id;
+  D_TYP : list il_id;
+  D_FUN : list il_id 
+  }
+.
+
+Fixpoint many_svars (xs : list (il_id * il_exp)) : il_subst :=
+  match xs with
+  | [] => subst_empty 
+  | (x, e) :: xs' => append_subst (subst_svar x e) (many_svars xs')
+  end
+.
+
+Fixpoint compose_substs (xs : list il_subst) : il_subst :=
+  match xs with
+  | [] => subst_empty
+  | x :: xs' => append_subst x (compose_substs xs')
+  end
+.
+
+Definition append_dom (d1 d2 : dom) : dom :=
+  {|
+  D_EXP := d1.(D_EXP) ++ d2.(D_EXP);
+  D_TYP := d1.(D_TYP) ++ d2.(D_TYP);
+  D_FUN := d1.(D_FUN) ++ d2.(D_FUN)
+  |}
+.
+
+Definition get_keys {A : Type} (s : StringMap.t A) : list string :=
+  List.map fst (StringMap.elements s).
+
+Definition dom_subst (s : il_subst) : dom :=
+  {| D_EXP := get_keys s.(S_EXP); D_TYP := get_keys s.(S_TYP); D_FUN := get_keys s.(S_FUN) |}.
+
+Definition bound_param (p : il_param) : dom :=
+  match p with
+  | ExpP il_id _ => {| D_EXP := [il_id]; D_TYP := []; D_FUN := [] |}
+  | TypP il_id => {| D_EXP := []; D_TYP := [il_id]; D_FUN := [] |}
+  | DefP il_id _ _ => {| D_EXP := []; D_TYP := []; D_FUN := [il_id]|}
+  end
+.
+
+Fixpoint bound_params (ps : list il_param) : dom :=
+  match ps with
+  | [] => {| D_EXP := []; D_TYP := []; D_FUN := [] |}
+  | p :: ps => append_dom (bound_param p) (bound_params ps)
+  end
+.
+
+(* TODO handle capture avoidance *)
+
+Definition subst_fun (s : il_subst) (x : il_id) : il_id :=
+  match StringMap.find x s.(S_FUN) with
+  | Some y => y
+  | None => x
+  end
+.
+
+
+
+Fixpoint subst_typ (s : il_subst) (t : il_typ) : il_typ :=
+  match t with
+  | VarT x args => 
+    match StringMap.find x s.(S_TYP) with
+    | Some t' => t'
+    | None => VarT x (List.map (subst_arg s) args)
+    end
+  | TupT xts => TupT (List.map (fun '(x, t) => (x, subst_typ s t)) xts)
+  | IterT t' it => IterT (subst_typ s t') (subst_iter s it)
+  | MatchT x args insts =>
+    MatchT x (List.map (subst_arg s) args) (List.map (fun '(qs, args', deftyp) =>
+      (List.map (subst_param s) qs, List.map (subst_arg s) args, subst_deftyp s deftyp)
+    ) insts)
+  | _ => t
+  end
+
+with
+
+subst_exp (s : il_subst) (e : il_exp) : il_exp :=
+  match e with
+  | VarE x => 
+    match StringMap.find x s.(S_EXP) with
+    | Some e' => e'
+    | _ => e
+    end
+  | UnE unop e1 => UnE unop (subst_exp s e1)
+  | BinE bop e1 e2 => BinE bop (subst_exp s e1) (subst_exp s e2)
+  | CmpE cmop e1 e2 => CmpE cmop (subst_exp s e1) (subst_exp s e2)
+  | TupE exps => TupE (List.map (subst_exp s) exps)
+  | CaseE m e' => CaseE m (subst_exp s e')
+  | OptE (Some e') => OptE (Some (subst_exp s e'))
+  | ListE exps => ListE (List.map (subst_exp s) exps)
+  | LiftE e' => LiftE (subst_exp s e')
+  | StrE efields => StrE (List.map (fun '(a, e) => (a, subst_exp s e))efields)
+  | ProjE e' n => ProjE (subst_exp s e') n
+  | LenE e' => LenE (subst_exp s e')
+  | MemE e1 e2 => MemE (subst_exp s e1) (subst_exp s e2)
+  | CatE e1 e2 => CatE (subst_exp s e1) (subst_exp s e2)
+  | IdxE e1 e2 => IdxE (subst_exp s e1) (subst_exp s e2)
+  | SliceE e1 e2 e3 => SliceE (subst_exp s e1) (subst_exp s e2) (subst_exp s e3)
+  | AccE e' p => AccE (subst_exp s e') (subst_path s p)
+  | UpdE e1 p e2 => UpdE (subst_exp s e1) (subst_path s p) (subst_exp s e2)
+  | ExtE e1 p e2 => ExtE (subst_exp s e1) (subst_path s p) (subst_exp s e2)
+  | CallE x args => CallE x (List.map (subst_arg s) args)
+  | IterE e' it xexps => IterE (subst_exp s e') (subst_iter s it) (List.map (fun '(x, t, e) => (x, subst_typ s t, subst_exp s e)) xexps)
+  | CvtE e' nt1 nt2 => CvtE (subst_exp s e') nt1 nt2
+  | SubE e' t1 t2 => SubE (subst_exp s e') (subst_typ s t1) (subst_typ s t2)
+  | MatchE args clauses =>
+    MatchE (List.map (subst_arg s) args) (List.map (fun '(qs, args', e, prems) =>
+      (List.map (subst_param s) qs, List.map (subst_arg s) args, subst_exp s e, List.map (subst_prem s) prems)
+    ) clauses)   
+  | _ => e
+  end
+
+with
+
+subst_path (s : il_subst) (p : il_path) : il_path :=
+  match p with
+  | RootP => RootP
+  | IdxP p' e' => IdxP (subst_path s p') (subst_exp s e')
+  | SliceP p' e1 e2 => SliceP (subst_path s p') (subst_exp s e1) (subst_exp s e2)
+  | DotP p' a => DotP (subst_path s p') a
+  | TheP p' => TheP (subst_path s p')
+  | UncaseP p' m => UncaseP (subst_path s p') m 
+  end
+
+with 
+
+subst_arg (s : il_subst) (a : il_arg) : il_arg :=
+  match a with
+  | ExpA e => ExpA (subst_exp s e)
+  | TypA t => TypA (subst_typ s t)
+  | DefA x => DefA (subst_fun s x)
+  end
+
+with
+
+subst_param (s : il_subst) (p : il_param) : il_param :=
+  match p with
+  | ExpP x t => ExpP x (subst_typ s t)
+  | TypP x => TypP x
+  | DefP x ps t => DefP x (List.map (subst_param s) ps) (subst_typ s t)
+  end
+with
+
+subst_iter (s : il_subst) (i : iter) : iter :=
+  match i with
+  | I_SUP x e => I_SUP x (subst_exp s e)
+  | _ => i
+  end
+
+
+with 
+
+subst_prem (s : il_subst) (p : il_prem) : il_prem :=
+  match p with
+  | RulePr x args e => RulePr x (List.map (subst_arg s) args) (subst_exp s e)
+  | IfPr e => IfPr (subst_exp s e)
+  | ElsePr => ElsePr
+  | LetPr e1 e2 => LetPr (subst_exp s e1) (subst_exp s e2)
+  | IterPr p' it xexps => IterPr (subst_prem s p') (subst_iter s it) (List.map (fun '(x, t, e) => (x, subst_typ s t, subst_exp s e)) xexps)
+  | NegPr p' => NegPr (subst_prem s p')
+  end
+
+with 
+
+subst_deftyp (s : il_subst) (dt : il_deftyp) : il_deftyp :=
+  match dt with
+  | AliasT t => AliasT (subst_typ s t)
+  | StructT typfields => StructT (List.map (fun '(a, qs, t, prems) =>
+    (a, List.map (subst_param s) qs, subst_typ s t, List.map (subst_prem s) prems) 
+  ) typfields)
+  | VariantT typcases => VariantT (List.map (fun '(m, qs, t, prems) =>
+    (m, List.map (subst_param s) qs, subst_typ s t, List.map (subst_prem s) prems) 
+  ) typcases)
+  end
+.
+
+
+Definition subst_quant (s : il_subst) (p : il_quant) : il_quant := subst_param s p.
+
+Definition arg_for_param (a : il_arg) (p : il_param) : il_subst :=
+  match a, p with
+  | ExpA e, ExpP x _ => {| S_EXP := singleton x e; S_TYP := empty_typ; S_FUN := empty_id |}
+  | TypA t, TypP x => {| S_EXP := empty_exp; S_TYP := singleton x t; S_FUN := empty_id |}
+  | DefA y, DefP x _ _ => {| S_EXP := empty_exp; S_TYP := empty_typ; S_FUN := singleton x y |} 
+  | _, _ => subst_empty
+  end
+.
+
+Fixpoint args_for_params (ags : list il_arg) (ps : list il_param) : il_subst :=
+  match ags, ps with
+  | [], [] => subst_empty
+  | _, [] => subst_empty
+  | [], _ => subst_empty
+  | a :: ags', p :: ps' => append_subst (arg_for_param a p) (args_for_params ags' ps')
+  end
+.
+
+Definition param_to_arg (p : il_param) : il_arg :=
+  match p with
+  | ExpP x _ => ExpA (VarE x)
+  | TypP x => TypA (VarT x [])
+  | DefP x _ _ => DefA x
+  end
+.
+
+Definition subst_argmatch (s : il_subst) (a : argmatch) : argmatch :=
+  match a with
+  | FailA => FailA
+  | MatchA a' a'' => MatchA (subst_arg s a') (subst_arg s a'')
+  end
+.
+
+Definition subst_expmatch (s : il_subst) (e : expmatch) : expmatch :=
+  match e with
+  | FailEM => FailEM
+  | MatchEM e' e'' => MatchEM (subst_exp s e') (subst_exp s e'')
+  end
+.
+
+Definition subst_rule (s : il_subst) (r : il_rule) : il_rule :=
+  match r with
+  | (qs, exp, prems) => (List.map (subst_param s) qs, subst_exp s exp, List.map (subst_prem s) prems)
+  end
+.
+
+(* TODO *)
+Inductive ok_subst : il_env -> il_subst -> list il_quant -> Prop := 
+  | Subst_OK : forall E s q_lst,
+    ok_subst E s q_lst.
+     
diff --git a/spectec/metatheory/theories/syntax.v b/spectec/metatheory/theories/syntax.v
new file mode 100644
index 0000000000..55d7abc0d8
--- /dev/null
+++ b/spectec/metatheory/theories/syntax.v
@@ -0,0 +1,230 @@
+From Stdlib Require Import List String.
+From mathcomp Require Import all_ssreflect all_algebra. 
+Import GRing.Theory.
+
+Parameter R : archiNumDomainType.
+
+(* SYNTAX *)
+
+Definition atom : Type := string.
+Definition mixop : Type := list (list atom).
+Definition il_id : Type := string.
+Definition text : Type := string.
+
+Inductive optyp : Type :=
+  | BoolOp
+  | NumOp
+.
+
+Inductive numunop : Type :=
+  | PlusOp
+  | MinusOp
+.
+
+Inductive boolunop : Type :=
+  | NotOp
+.
+
+Inductive unop : Type :=
+  | NumUnop : numunop -> unop
+  | BoolUnop : boolunop -> unop
+.
+
+Inductive numbinop : Type :=
+  | AddOp
+  | SubOp
+  | MulOp
+  | DivOp
+  | ModOp
+  | PowOp
+.
+
+Inductive boolbinop : Type :=
+  | AndOp
+  | OrOp
+  | ImplOp
+  | EquivOp
+.
+
+Inductive binop : Type :=
+  | NumBinop : numbinop -> binop
+  | BoolBinop : boolbinop -> binop
+.
+
+Inductive numcmpop : Type :=
+  | LtOp
+  | LeOp
+  | GtOp
+  | GeOp
+.
+
+Inductive boolcmpop : Type :=
+  | EqOp
+  | NeqOp
+.
+
+Inductive cmpop : Type :=
+  | NumCmpop : numcmpop -> cmpop
+  | BoolCmpop : boolcmpop -> cmpop
+.
+
+Inductive numtyp : Type :=
+  | NatT
+  | IntT
+  | RatT
+  | RealT
+.
+
+Inductive il_num : Type :=
+  | NatE : nat -> il_num
+  | IntE : int -> il_num
+  | RatE : rat -> il_num
+  | RealE : R -> il_num
+.
+
+Inductive il_val : Type :=
+  | NumV : il_num -> il_val
+  | BoolV : bool -> il_val
+  | TextV : text -> il_val
+  | TupV : list il_val -> il_val
+  | CaseV : mixop -> il_val -> il_val
+  | OptV : option il_val -> il_val
+  | ListV : list il_val -> il_val
+  | StrV : list (atom * il_val) -> il_val
+.
+
+Inductive il_typ : Type :=
+  | VarT : il_id -> list il_arg -> il_typ
+  | BoolT
+  | TextT
+  | NumT : numtyp -> il_typ
+  | TupT : list (il_id * il_typ) -> il_typ
+  | IterT : il_typ -> iter -> il_typ
+  | MatchT : il_id -> list il_arg -> list (list il_param * list il_arg * il_deftyp) -> il_typ
+
+with
+
+il_exp : Type :=
+  | VarE : il_id -> il_exp
+  | BoolE : bool -> il_exp
+  | NumE : il_num -> il_exp
+  | TextE : text -> il_exp
+  | UnE : unop -> il_exp -> il_exp
+  | BinE : binop -> il_exp -> il_exp -> il_exp
+  | CmpE : cmpop -> il_exp -> il_exp -> il_exp
+  | TupE : list il_exp -> il_exp
+  | ProjE : il_exp -> nat -> il_exp
+  | CaseE : mixop -> il_exp -> il_exp
+  | OptE : option il_exp -> il_exp
+  | StrE : list (atom * il_exp) -> il_exp
+  | DotE : il_exp * atom -> il_exp
+  | ListE : list il_exp -> il_exp
+  | LiftE : il_exp -> il_exp
+  | MemE : il_exp -> il_exp -> il_exp
+  | LenE : il_exp -> il_exp
+  | CatE : il_exp -> il_exp -> il_exp
+  | IdxE : il_exp -> il_exp -> il_exp
+  | SliceE : il_exp -> il_exp -> il_exp -> il_exp
+  | AccE : il_exp -> il_path -> il_exp
+  | UpdE : il_exp -> il_path -> il_exp -> il_exp
+  | ExtE : il_exp -> il_path -> il_exp -> il_exp
+  | CallE : il_id -> list il_arg -> il_exp
+  | IterE : il_exp -> iter -> list (il_id * il_typ * il_exp) -> il_exp
+  | CvtE : il_exp -> numtyp -> numtyp -> il_exp
+  | SubE : il_exp -> il_typ -> il_typ -> il_exp
+  | IfE : il_exp -> il_exp -> il_exp -> il_exp
+  | MatchE : list il_arg -> list (list il_param * list il_arg * il_exp * list il_prem) -> il_exp
+
+with
+
+il_path : Type :=
+  | RootP
+  | IdxP : il_path -> il_exp -> il_path
+  | TheP : il_path -> il_path
+  | UncaseP : il_path -> mixop -> il_path 
+  | SliceP : il_path -> il_exp -> il_exp -> il_path
+  | DotP : il_path -> atom -> il_path
+
+with
+
+il_arg : Type := 
+  | ExpA : il_exp -> il_arg
+  | TypA : il_typ -> il_arg
+  | DefA : il_id -> il_arg
+
+with
+
+iter : Type :=
+  | I_STAR
+  | I_OPT
+  | I_PLUS
+  | I_SUP : il_id -> il_exp -> iter
+
+with 
+
+il_param : Type :=
+  | ExpP : il_id -> il_typ -> il_param
+  | TypP : il_id -> il_param
+  | DefP : il_id -> list il_param -> il_typ -> il_param
+
+with 
+
+il_prem : Type :=
+  | RulePr : il_id -> list il_arg -> il_exp -> il_prem
+  | IfPr : il_exp -> il_prem
+  | ElsePr
+  | LetPr : il_exp -> il_exp -> il_prem
+  | IterPr : il_prem -> iter -> list (il_id * il_typ * il_exp) -> il_prem
+  | NegPr : il_prem -> il_prem
+
+with 
+
+il_deftyp : Type :=
+  | AliasT : il_typ -> il_deftyp
+  | StructT : list (atom * list il_param * il_typ * list il_prem) -> il_deftyp
+  | VariantT : list (mixop * list il_param * il_typ * list il_prem) -> il_deftyp
+.
+
+Definition exppull : Type := (il_id * il_typ * il_exp).
+Definition il_quant : Type := il_param.
+Definition typfield : Type := atom * list il_quant * il_typ * list il_prem.
+Definition typcase : Type := mixop * list il_quant * il_typ * list il_prem.
+
+Definition expfield : Type := atom * il_exp.
+
+Definition il_inst : Type := list il_quant * list il_arg * il_deftyp.
+Definition il_rule : Type := list il_quant * il_exp * list il_prem.
+Definition il_clause : Type := list il_quant * list il_arg * il_exp * list il_prem.
+
+Inductive il_def : Type :=
+  | TypD : il_id -> list il_param -> list il_inst -> il_def
+  | RelD : il_id -> list il_param -> il_typ -> list il_rule -> il_def
+  | DecD : il_id -> list il_param -> il_typ -> list il_clause -> il_def
+  | RecD : list il_def -> il_def
+.
+
+Definition script : Type := list il_def.
+
+Fixpoint val_to_exp (v : il_val) : il_exp :=
+  match v with
+  | NumV n => NumE n
+  | BoolV b => BoolE b
+  | TextV t => TextE t
+  | TupV vs => TupE (List.map val_to_exp vs)
+  | CaseV m v => CaseE m (val_to_exp v)
+  | OptV (Some v) => OptE (Some (val_to_exp v))
+  | OptV None => OptE None
+  | ListV vs => ListE (List.map val_to_exp vs)
+  | StrV valfields => StrE (List.map (fun '(a, v) => (a, val_to_exp v)) valfields)
+  end
+.
+
+Inductive argmatch : Type :=
+  | MatchA : il_arg -> il_arg -> argmatch
+  | FailA : argmatch
+.
+
+Inductive expmatch : Type :=
+  | MatchEM : il_exp -> il_exp -> expmatch
+  | FailEM : expmatch
+.
\ No newline at end of file
diff --git a/spectec/metatheory/theories/typing.v b/spectec/metatheory/theories/typing.v
new file mode 100644
index 0000000000..af3d0bb75f
--- /dev/null
+++ b/spectec/metatheory/theories/typing.v
@@ -0,0 +1,437 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import all_ssreflect all_algebra.
+From MetaSpectec Require Import syntax env reduction subst utils.
+Import ListNotations.
+Open Scope env_scope.
+
+Inductive catable_typ : il_env -> il_typ -> Prop :=
+  | ct_iter : forall env t t' it,
+    expand_typ (env_to_store env) t (AliasT (IterT t' it)) ->
+    catable_typ env t
+  | ct_struct : forall env t typfields,
+    expand_typ (env_to_store env) t (StructT typfields) ->
+    List.Forall (fun p => catable_typ env (snd (fst p))) typfields ->
+    catable_typ env t
+.
+
+Inductive sub_numtyp : numtyp -> numtyp -> Prop :=
+  | sn_nat : sub_numtyp NatT IntT
+  | sn_int : sub_numtyp IntT RatT
+  | sn_rat : sub_numtyp RatT RealT
+  | sn_rfl : forall nt, sub_numtyp nt nt
+  | sn_trans : forall nt1 nt2 nt,
+    sub_numtyp nt1 nt ->
+    sub_numtyp nt nt2 ->
+    sub_numtyp nt1 nt2
+.
+
+Inductive sub_param : il_env -> il_param -> il_param -> il_subst -> Prop :=
+  | sp_exp : forall env x1 t1 x2 t2,
+    sub_typ env t1 t2 ->
+    sub_param env (ExpP x1 t1) (ExpP x2 t2) (subst_svar x2 (VarE x1))
+  | sp_typ : forall env x1 x2,
+    sub_param env (TypP x1) (TypP x2) (subst_styp x2 (VarT x1 []))
+  | sp_fun : forall env x1 ps1 t1 x2 ps2 t2 sbst,
+    let penv2 := paramenv ps2 in
+    sub_params env ps2 ps1 sbst ->
+    sub_typ (env @@ penv2) (subst_typ sbst t1) t2 ->
+    sub_param env (DefP x1 ps1 t1) (DefP x2 ps2 t2) (subst_sfun x2 x1)
+
+with
+
+sub_params : il_env -> list il_param -> list il_param -> il_subst -> Prop :=
+  | sps_emp : forall env, sub_params env [] [] subst_empty
+  | sps_cons : forall env p1 p1s p2 p2s sbst sbst',
+    sub_param env p1 p2 sbst ->
+    sub_params env p1s (List.map (subst_param sbst) p2s) sbst' ->
+    sub_params env (p1 :: p1s) (p2 :: p2s) (append_subst sbst sbst')
+.
+
+
+Inductive ok_numunop : numunop -> numtyp -> numtyp -> Prop :=
+  | ok_unop_sign : forall numop nt,
+    sub_numtyp IntT nt ->
+    ok_numunop numop nt nt
+.
+
+Inductive ok_numbinop : numbinop -> numtyp -> numtyp -> numtyp -> Prop :=
+  | ok_binop_add : forall nt, ok_numbinop AddOp nt nt nt
+  | ok_binop_sub : forall nt nt',
+    sub_numtyp IntT nt' ->
+    ok_numbinop SubOp nt nt nt'
+  | ok_binop_mul : forall nt, ok_numbinop MulOp nt nt nt
+  | ok_binop_div : forall nt nt',
+    sub_numtyp RatT nt' ->
+    ok_numbinop DivOp nt nt nt'
+  | ok_binop_mod : forall nt,
+    sub_numtyp nt IntT ->
+    ok_numbinop ModOp nt nt nt
+  | ok_binop_pownat : forall nt, ok_numbinop PowOp nt NatT nt
+  | ok_binop_powint : forall nt,
+    sub_numtyp nt RatT ->
+    ok_numbinop PowOp nt IntT nt
+.
+
+Inductive ok_exp: il_env -> il_exp -> il_typ -> Prop :=
+  | oke_bool : forall env b, ok_exp env (BoolE b) BoolT
+  | oke_nat : forall env n, ok_exp env (NumE (NatE n)) (NumT NatT)
+  | oke_int : forall env i, ok_exp env (NumE (IntE i)) (NumT IntT)
+  | oke_rat : forall env q, ok_exp env (NumE (RatE q)) (NumT RatT)
+  | oke_real : forall env r, ok_exp env (NumE (RealE r)) (NumT RealT)
+  | oke_text : forall env t, ok_exp env (TextE t) TextT
+  | oke_unop_bool : forall env bop e,
+    ok_exp env e BoolT ->
+    ok_exp env (UnE (BoolUnop bop) e) BoolT
+  | oke_unop_num : forall env numop e nt nt',
+    ok_exp env e (NumT nt) ->
+    ok_numunop numop nt nt' ->
+    ok_exp env (UnE (NumUnop numop) e) (NumT nt')
+  | oke_binop_bool : forall env bop e1 e2,
+    ok_exp env e1 BoolT ->
+    ok_exp env e2 BoolT ->
+    ok_exp env (BinE (BoolBinop bop) e1 e2) BoolT
+  | oke_binop_num : forall env numop e1 e2 nt1 nt2 nt,
+    ok_exp env e1 (NumT nt1) ->
+    ok_exp env e2 (NumT nt2) ->
+    ok_numbinop numop nt1 nt2 nt ->
+    ok_exp env (BinE (NumBinop numop) e1 e2) (NumT nt)
+  | oke_cmp_bool : forall env bop e1 e2 t,
+    ok_exp env e1 t ->
+    ok_exp env e2 t ->
+    ok_exp env (CmpE (BoolCmpop bop) e1 e2) BoolT
+  | oke_cmp_num : forall env numop e1 e2 nt,
+    ok_exp env e1 (NumT nt) ->
+    ok_exp env e2 (NumT nt) ->
+    ok_exp env (CmpE (NumCmpop numop) e1 e2) BoolT
+  | oke_tup_eps : forall env, ok_exp env (TupE []) (TupT [])
+  | oke_tup_cons : forall env e1 es x1 t1 tups,
+    let sbst := (subst_svar x1 e1) in
+    ok_exp env e1 t1 ->
+    ok_exp env (TupE es) (subst_typ sbst (TupT tups)) ->
+    ok_exp env (TupE (e1 :: es)) (TupT ((x1, t1) :: tups))
+  | oke_opt : forall env e_opt t,
+    option_forall (fun e => ok_exp env e t) e_opt ->
+    ok_exp env (OptE e_opt) (IterT t I_OPT)
+  | oke_list : forall env es t,
+    List.Forall (fun e => ok_exp env e t) es ->
+    ok_exp env (ListE es) (IterT t I_STAR)
+  | oke_lift : forall env e t,
+    ok_exp env e (IterT t I_OPT) ->
+    ok_exp env (LiftE e) (IterT t I_STAR)
+  | oke_case : forall env m e x ags tcs t qs ps,
+    expand_typ (env_to_store env) (VarT x ags) (VariantT tcs) ->
+    List.In (m, qs, t, ps) tcs ->
+    ok_exp env e t ->
+    ok_exp env (CaseE m e) (VarT x ags)
+  | oke_str : forall env a e x ags tfs fs t qs ps,
+    expand_typ (env_to_store env) (VarT x ags) (StructT tfs) ->
+    size tfs = size fs ->
+    List.In (a, qs, t, ps) tfs ->
+    List.In (a, e) fs ->
+    ok_exp env e t ->
+    ok_exp env (StrE fs) (VarT x ags)
+  (* TODO rule for ProjE *)
+  | oke_len : forall env e t,
+    ok_exp env e (IterT t I_STAR) ->
+    ok_exp env (LenE e) (NumT NatT)
+  | oke_mem : forall env e1 e2 t1,
+    ok_exp env e1 t1 ->
+    ok_exp env e2 (IterT t1 I_STAR) ->
+    ok_exp env (MemE e1 e2) BoolT
+  | oke_cat : forall env e1 e2 t,
+    ok_exp env e1 (IterT t I_STAR) ->
+    ok_exp env e2 (IterT t I_STAR) ->
+    catable_typ env t ->
+    ok_exp env (CatE e1 e2) (IterT t I_STAR)
+  | oke_acc : forall env e p t t',
+    ok_exp env e t ->
+    ok_path env p t t' ->
+    ok_exp env (AccE e p) t'
+  | oke_upd : forall env e1 p e2 t1 t2,
+    ok_exp env e1 t1 ->
+    ok_exp env e2 t2 ->
+    ok_path env p t1 t2 ->
+    ok_exp env (UpdE e1 p e2) t1
+  | oke_ext : forall env e1 p e2 t1 t2,
+    ok_exp env e1 t1 ->
+    ok_exp env e2 (IterT t2 I_STAR) ->
+    ok_path env p t1 (IterT t2 I_STAR) ->
+    ok_exp env (ExtE e1 p e2) t1
+  | oke_call : forall env x ags ps sbst rt clauses,
+    StringMap.find x (DEFS env) = Some (ps, rt, clauses) ->
+    ok_args env ags ps sbst ->
+    ok_exp env (CallE x ags) (subst_typ sbst rt)
+  | oke_iter : forall env env' e iter xps t iter',
+    ok_iter env iter iter' env' ->
+    List.Forall (fun p => ok_typ env (snd (fst p))) xps ->
+    List.Forall (fun p => ok_exp env (snd p) (IterT (snd (fst p)) iter')) xps ->
+    let envs := many_vars (List.map fst xps) in
+    ok_exp (env @@ envs @@ env') e t ->
+    ok_typ env t ->
+    ok_exp env (IterE e iter xps) (IterT t iter')
+  | oke_cvt : forall env e nt1 nt2,
+    ok_exp env e (NumT nt1) ->
+    ok_exp env (CvtE e nt1 nt2) (NumT nt2)
+  | oke_sub : forall env e t1 t2, 
+    ok_exp env e t1 ->
+    sub_typ env t1 t2 ->
+    ok_exp env (SubE e t1 t2) t2
+  | oke_match : forall env ags ps clauses t sbst,
+    ok_args env ags ps sbst -> 
+    ok_params env ps ->
+    let penv := paramenv ps in 
+    List.Forall (fun c => ok_clause (append_env env penv) c ps t) clauses ->
+    ok_exp env (MatchE ags clauses) t
+  | ok_exp_conv : forall env e t t',
+    ok_exp env e t' ->
+    eq_typ (env_to_store env) t t' ->
+    ok_exp env e t
+
+with
+
+ok_path : il_env -> il_path -> il_typ -> il_typ -> Prop :=
+  | okp_root : forall env t,
+    ok_typ env t ->
+    ok_path env RootP t t
+  | okp_the : forall env p t t',
+    ok_path env p t (IterT t' I_OPT) ->
+    ok_path env (TheP p) t t'
+  | okp_idx : forall env p e t t',
+    ok_path env p t (IterT t' I_STAR) ->
+    ok_exp env e (NumT NatT) ->
+    ok_path env (IdxP p e) t t'
+  | okp_slice : forall env p e1 e2 t t',
+    ok_path env p t (IterT t' I_STAR) ->
+    ok_exp env e1 (NumT NatT) ->
+    ok_exp env e2 (NumT NatT) ->
+    ok_path env (SliceP p e1 e2) t t'
+  | okp_dot : forall env p a x ags t t' tfs qs prems,
+    ok_path env p t (VarT x ags) -> 
+    expand_typ (env_to_store env) (VarT x ags) (StructT tfs) ->
+    List.In (a, qs, t', prems) tfs ->
+    ok_path env (DotP p a) t t'
+  | okp_uncase : forall env p m t t' x ags qs prems tcs,
+    ok_path env p t (VarT x ags) ->
+    expand_typ (env_to_store env) (VarT x ags) (VariantT tcs) ->
+    List.In (m, qs, t', prems) tcs ->
+    ok_path env (UncaseP p m) t t'
+  | okp_conv : forall env p t t' t'',
+    ok_path env p t'' t' ->
+    eq_typ (env_to_store env) t t'' ->
+    ok_path env p t t'
+
+with
+
+ok_typ : il_env -> il_typ -> Prop :=
+  | okt_bool : forall env, ok_typ env BoolT
+  | okt_num : forall env nt, ok_typ env (NumT nt)
+  | okt_text : forall env, ok_typ env TextT
+  | okt_tupemp : forall env, ok_typ env (TupT [])
+  | okt_tup : forall env x1 t1 tups,
+    let env' := single_var x1 t1 in
+    ok_typ env t1 ->
+    ok_typ (env @@ env') (TupT tups) ->
+    ok_typ env (TupT ((x1, t1) :: tups))
+  | okt_iter : forall env t it,
+    ok_typ env t ->
+    (it = I_STAR) \/ (it = I_OPT) ->
+    ok_typ env (IterT t it)
+  | okt_var : forall env x ags ps insts sbst,
+    (StringMap.find x (TYPS env) = Some (ps, insts)) -> 
+    ok_args env ags ps sbst ->
+    ok_typ env (VarT x ags)
+  | okt_match : forall env x ags ps insts sbst,
+    (StringMap.find x (TYPS env) = Some (ps, insts)) -> 
+    ok_args env ags ps sbst ->
+    List.Forall (fun inst => ok_inst env inst ps) insts ->
+    ok_typ env (MatchT x ags insts)
+
+with
+
+ok_iter : il_env -> iter -> iter -> il_env -> Prop :=
+  | oki_quest : forall env, ok_iter env I_OPT I_OPT env_empty 
+  | oki_star : forall env, ok_iter env I_STAR I_STAR env_empty
+  | oki_plus : forall env, ok_iter env I_PLUS I_STAR env_empty
+  | oki_sup_some : forall env e x,
+    ok_exp env e (NumT NatT) ->
+    ok_iter env (I_SUP x e) I_STAR (single_var x (NumT NatT))
+
+with
+
+ok_prem : il_env -> il_prem -> Prop :=
+  | okp_rule : forall env x ags sbst e ps t rules,
+    StringMap.find x (RELS env) = Some (ps, t, rules) ->
+    ok_args env ags ps sbst ->
+    ok_exp env e (subst_typ sbst t) ->
+    ok_prem env (RulePr x ags e)
+  | okp_if : forall env e,
+    ok_exp env e BoolT ->
+    ok_prem env (IfPr e)
+  | okp_else : forall env, ok_prem env ElsePr
+  (* TODO think about let semantics *)
+  | okp_let : forall env e1 e2 t,
+    ok_exp env e1 t ->
+    ok_exp env e2 t ->
+    ok_prem env (LetPr e1 e2)
+  | okp_iter : forall env pr it it' env' xps,
+    ok_iter env it it' env' ->
+    List.Forall (fun p => ok_typ env (snd (fst p))) xps ->
+    List.Forall (fun p => ok_exp env (snd p) (IterT (snd (fst p)) it')) xps ->
+    let envs := many_vars (List.map fst xps) in
+    ok_prem (env @@ envs @@ env') pr ->
+    ok_prem env (IterPr pr it xps)
+  | okp_neg : forall env p,
+    ok_prem env p ->
+    ok_prem env (NegPr p)
+
+with
+
+ok_arg : il_env -> il_arg -> il_param -> il_subst -> Prop :=
+  | oka_exp : forall env e x t,
+    ok_exp env e t ->
+    ok_arg env (ExpA e) (ExpP x t) (subst_svar x e)
+  | oka_typ : forall env t x,
+    ok_typ env t ->
+    ok_arg env (TypA t) (TypP x) (subst_styp x t)
+  | oka_fun : forall env y x ps rt ps' rt' clauses sbst,
+    StringMap.find y (DEFS env) = Some (ps', rt', clauses) ->
+    sub_params env ps ps' sbst ->
+    sub_typ env (subst_typ sbst rt') rt ->
+    ok_arg env (DefA y) (DefP x ps rt) (subst_sfun x y)
+
+with
+
+ok_args : il_env -> list il_arg -> list il_param -> il_subst -> Prop :=
+  | okas_emp : forall env, ok_args env [] [] subst_empty
+  | okas_cons : forall env a1 p1 sbst sbst1 ags ps,
+    ok_arg env a1 p1 sbst1 ->
+    ok_args env ags (List.map (subst_param sbst) ps) sbst ->
+    ok_args env (a1 :: ags) (p1 :: ps) (append_subst sbst1 sbst)
+
+with
+
+ok_param : il_env -> il_param -> Prop :=
+  | okpa_exp : forall env x t,
+    ok_typ env t ->
+    ok_param env (ExpP x t) 
+  | okpa_typ : forall env x, ok_param env (TypP x)
+  | okpa_fun : forall env x ps t, 
+    let penv := paramenv ps in
+    ok_params env ps ->
+    ok_typ (env @@ penv) t ->
+    ok_param env (DefP x ps t)
+
+with
+
+ok_params : il_env -> list il_param -> Prop :=
+  | okpas_emp : forall env, ok_params env []
+  | okpas_cons : forall env p1 ps,
+    ok_param env p1 ->
+    ok_params (env @@ (paramenv [p1])) ps
+
+with
+
+ok_typfield : il_env -> typfield -> Prop :=
+  | oktypfield : forall env a t qs prems,
+    let tenv := tupenv t in
+    let qsenv := paramenv qs in
+    ok_typ env t ->
+    ok_params (env @@ tenv) qs ->
+    List.Forall (fun p => ok_prem (env @@ tenv @@ qsenv) p) prems ->
+    ok_typfield env (a, qs, t, prems)
+
+with
+
+ok_typcase : il_env -> typcase -> Prop :=
+  | oktypcase : forall env m t qs prems,
+    let tenv := tupenv t in
+    let qsenv := paramenv qs in
+    ok_typ env t ->
+    ok_params (env @@ tenv) qs ->
+    List.Forall (fun p => ok_prem (env @@ tenv @@ qsenv) p) prems ->
+    ok_typcase env (m, qs, t, prems)
+
+with
+
+ok_deftyp : il_env -> il_deftyp -> Prop :=
+  | okd_alias : forall env t,
+    ok_typ env t ->
+    ok_deftyp env (AliasT t)
+  | okd_struct : forall env tfs,
+    let atoms := List.map (fun '(a, qs, t, prems) => a) tfs in
+    List.Forall (fun tf => ok_typfield env tf) tfs ->
+    disjoint atoms ->
+    ok_deftyp env (StructT tfs)
+  | okd_variant : forall env tcs,
+    let mixops := List.map (fun '(m, qs, t, prems) => m) tcs in
+    List.Forall (fun tc => ok_typcase env tc) tcs ->
+    disjoint mixops ->
+    ok_deftyp env (VariantT tcs)
+
+with 
+
+ok_inst : il_env -> il_inst -> list il_param -> Prop :=
+  | oki_inst : forall env qs ags dt ps sbst,
+    ok_params env qs ->
+    ok_args (env @@ (paramenv qs)) ags ps sbst ->
+    ok_deftyp (env @@ (paramenv qs)) dt ->
+    ok_inst env (qs, ags, dt) ps
+
+with
+
+ok_clause : il_env -> il_clause -> list il_param -> il_typ -> Prop :=
+  | okc_clause : forall env qs ags e prems ps t sbst,
+    let qsenv := paramenv qs in
+    ok_params env qs ->
+    ok_args (env @@ qsenv) ags ps sbst ->
+    ok_exp (env @@ qsenv) e t ->
+    List.Forall (fun p => ok_prem (env @@ qsenv) p) prems ->
+    ok_clause env (qs, ags, e, prems) ps t
+.
+
+Inductive ok_rule : il_env -> il_rule -> il_typ -> Prop :=
+  | okr_rule : forall env qs e prems t,
+    ok_params env qs ->
+    ok_exp (env @@ (paramenv qs)) e t ->
+    List.Forall (fun p => ok_prem (env @@ (paramenv qs)) p) prems ->
+    ok_rule env (qs, e, prems) t
+.
+
+Inductive ok_def : il_env -> il_def -> il_env -> Prop :=
+  | okd_typ : forall env x ps insts,
+    let env' := single_envtyp x ps insts in
+    ok_params env ps ->
+    List.Forall (fun inst => ok_inst env inst ps) insts ->
+    ok_def env (TypD x ps insts) (env @@ env')
+  | okd_rel : forall env x ps t rules,
+    let env' := single_rel x ps t rules in
+    let penv := paramenv ps in
+    ok_params env ps ->
+    List.Forall (fun rule => ok_rule (env @@ penv) rule t) rules ->
+    ok_def env (RelD x ps t rules) (env @@ env')
+  | okd_fun : forall env x ps t clauses,
+    let env' := single_def x ps t clauses in
+    let penv := paramenv ps in
+    ok_params env ps ->
+    List.Forall (fun clause => ok_clause (env @@ penv) clause ps t) clauses ->
+    ok_def env (DecD x ps t clauses) (env @@ env')
+  (* TODO recs doesn't make much sense *)
+  | okd_rec : forall env env' defs,
+    ok_defs (env @@ env') defs env' ->
+    ok_def env (RecD defs) env'
+  
+with
+
+ok_defs : il_env -> list il_def -> il_env -> Prop :=
+  | okdefs_emp : forall env, ok_defs env [] env_empty
+  | okdefs_cons : forall env d1 defs env' env'', 
+    ok_def env d1 env' ->
+    ok_defs env' defs env'' ->
+    ok_defs env (d1 :: defs) env''
+.
+
+Inductive ok_script : script -> Prop :=
+  | okscript : forall defs env,
+    ok_defs env_empty defs env ->
+    ok_script defs
+.
diff --git a/spectec/metatheory/theories/utils.v b/spectec/metatheory/theories/utils.v
new file mode 100644
index 0000000000..5e4be81264
--- /dev/null
+++ b/spectec/metatheory/theories/utils.v
@@ -0,0 +1,193 @@
+From Stdlib Require Import List String Reals.
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool seq eqtype rat ssrint.
+Import ListNotations.
+From MetaSpectec Require Import syntax.
+From HB Require Import structures.
+
+Inductive option_forall {T : Type} (P : (T -> Prop)) : option T -> Prop :=
+	| opt_none : option_forall P None
+  | opt_some : forall x,
+    P x ->
+    option_forall P (Some x)
+.
+
+Definition opt_to_lst {X : Type} (x : option X) : list X :=
+  match x with
+  | Some a => [a]
+  | None => []
+  end
+.
+
+(* PRE: size xs <= 1 *)
+Definition lst_to_opt {X : Type} (xs : list X) : option X :=
+  match xs with
+  | [] => None
+  | [x] => Some x
+  (* Should not happen *)
+  | _ => None
+  end
+.
+
+Definition option_map {X Y : Type} (f : X -> Y) (x_opt : option X) : option Y :=
+  match x_opt with
+  | Some x => Some (f x)
+  | None => None
+  end
+.
+
+Definition same_opt {X : Type} (x_opt : option X) (y_opt : option X) : bool :=
+  match x_opt, y_opt with
+  | Some _, Some _ => true
+  | None, None => true
+  | _, _ => false
+  end
+.
+
+Definition list_zipWith {X Y Z : Type} (f : X -> Y -> Z) (xs : seq X) (ys : seq Y) : seq Z :=
+	seq.map (fun '(x, y) => f x y) (seq.zip xs ys).
+
+Definition slice {A : Type} (i j : nat) (l : list A) : list A :=
+  firstn (j - i) (skipn i l).
+
+(* PRE: i < size l *)
+Definition update {A : Type} (l : list A) (i : nat) (x : A) : list A :=
+  set_nth x l i x.
+
+Definition update_slice {A : Type} (l : list A) (i : nat) (j : nat) (xs : list A) : list A :=
+  let idx_lst := iota i (j - i) in
+  foldl (fun acc '(idx, x) => update acc idx x) l (zip idx_lst xs)
+.
+
+Definition is_plaintyp (t : il_typ) : bool :=
+  match t with
+  | VarT _ _ => false
+  | _ => true
+  end
+.
+
+Fixpoint disjoint {X : eqType} (xs : list X) : bool :=
+  match xs with
+  | [] => true
+  | x :: xs => negb (x \in xs) && disjoint xs
+  end
+.
+
+Definition same_size {X : Type} (xss : list (list X)) : bool :=
+  match xss with
+  | [] => true
+  | [_] => true
+  | xs :: xss' => seq.all (fun xs' => size xs == size xs') xss'
+  end
+.
+
+(* PRE: all lists in xss are of same size *)
+Fixpoint transpose_helper {X : Type} (xss : list (list X)) (n : nat) : list (list X) :=
+  match n with
+  | O => []
+  | S n' =>
+    let heads := (List.flat_map (fun xs => 
+      match xs with
+      | [] => []
+      | x :: xs' => [x]
+      end
+    ) xss) in
+    heads :: transpose_helper (List.map behead xss) n'
+  end
+.
+
+Definition transpose {X : Type} (xss : list (list X)) : list (list X) :=
+  match xss with
+  | [] => []
+  | (xs :: xss') => transpose_helper xss (size xs)
+  end
+.
+
+Definition transpose_opt {X : Type} (xss : option (list X)) : list (option X) :=
+  match xss with
+  | None => []
+  | Some xss' => List.map (fun x => Some x) xss'
+  end
+.
+
+Definition is_expmatch (x : argmatch) : bool :=
+  match x with
+  | MatchA (ExpA _) (ExpA _) => true
+  | _ => false
+  end
+.
+
+Definition to_argmatch (x : expmatch) : argmatch :=
+  match x with
+  | FailEM => FailA
+  | MatchEM e e' => MatchA (ExpA e) (ExpA e')
+  end
+.
+
+Definition list_mapi {X Y : Type} (f : nat -> X -> Y) (xs : list X) : list Y :=
+  let idxs := iota 0 (size xs) in
+  List.map (fun '(i, x) => f i x) (zip idxs xs)
+.
+
+Inductive List_Forall3 {A B C: Type} (R : A -> B -> C -> Prop): seq A -> seq B -> seq C -> Prop :=
+	| Forall3_nil : List_Forall3 R nil nil nil
+	| Forall3_cons : forall x y z l l' l'',
+		R x y z -> List_Forall3 R l l' l'' -> List_Forall3 R (x :: l) (y :: l') (z :: l'')
+.
+
+Definition list_map3 {A B C D: Type} (f : A -> B -> C -> D) (xs : seq A) (ys : seq B) (zs : seq C) : seq D :=
+	seq.map (fun '(x, (y, z)) => f x y z) (seq.zip xs (seq.zip ys zs))
+.
+
+Definition atomtyp (x : typfield) : atom * il_typ :=
+  match x with
+  | (a, _, t, _) => (a, t)
+  end
+.
+
+Definition atomtyps (xs : list typfield) : list (atom * il_typ) :=
+  List.map atomtyp xs
+.
+
+Definition exp_from_field (x : expfield) : il_exp :=
+  match x with
+  | (a, e) => e
+  end
+.
+
+(* Decidable equality axiom *)
+
+Lemma eq_dec_Equality_axiom :
+  forall (T : Type) (eq_dec : forall (x y : T), decidable (x = y)),
+  let eqb v1 v2 := is_left (eq_dec v1 v2) in Equality.axiom eqb.
+Proof.
+  move=> T eq_dec eqb x y. rewrite /eqb.
+  case: (eq_dec x y); by [apply: ReflectT | apply: ReflectF].
+Qed.
+
+(* Decidable equality for atoms *)
+
+Definition atom_eq_dec : forall (v1 v2 : atom),
+  {v1 = v2} + {v1 <> v2}.
+Proof. do ? decide equality. Defined.
+
+Definition atom_eqb (v1 v2 : atom) : bool :=
+	is_left(atom_eq_dec v1 v2).
+Definition eqatomP : Equality.axiom (atom_eqb) :=
+	eq_dec_Equality_axiom (atom) (atom_eq_dec).
+
+HB.instance Definition _ := hasDecEq.Build (atom) (eqatomP).
+
+(* Decidable equality for mixops *)
+
+Definition mixop_eq_dec : forall (v1 v2 : mixop),
+  {v1 = v2} + {v1 <> v2}.
+Proof. do ? decide equality. Defined.
+
+Definition mixop_eqb (v1 v2 : mixop) : bool :=
+	is_left(mixop_eq_dec v1 v2).
+Definition eqmixopP : Equality.axiom (mixop_eqb) :=
+	eq_dec_Equality_axiom (mixop) (mixop_eq_dec).
+
+HB.instance Definition _ := hasDecEq.Build (mixop) (eqmixopP).
+
+