diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
index 260771e..6e3fcb5 100644
--- a/Lampe/Lampe.lean
+++ b/Lampe/Lampe.lean
@@ -269,15 +269,44 @@ nr_def call_decl<>(x: Field, y : Field) -> Field {
    STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
      ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
   simp only [call_decl, struct_construct]
-  steps <;> tauto
-  . simp_all [exists_const, SLP.true_star]
+  apply STHoare.letIn_intro
+  on_goal 3 => exact (fun (v : Tp.denote p $ .tuple _ [.field, .field]) => v = (x, y, ()))
+  apply STHoare.callDecl_intro <;> tauto
+  . apply STHoare.letIn_intro
+    . steps
+    . intros
+      steps
+      aesop
+  . intros
     steps
-    simp_all [exists_const, SLP.true_star]
-    simp_all [SLP.entails, SLP.wand, SLP.star, SLP.lift, SLP.forall']
-    intros
-    exists ∅, ∅
-    simp_all
-    apply And.intro rfl ?_
-    exists ∅, ∅
-    simp_all
-    apply And.intro rfl rfl
+    aesop
+
+
+nr_def simple_tuple<>() -> Field {
+  let t = `(1 : Field, true, 3 : Field);
+  t.2 : Field
+}
+
+example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 3) := by
+  simp only [simple_tuple]
+  steps
+  aesop
+
+nr_def simple_slice<>() -> bool {
+  let s = &[true, false];
+  s[[1 : u32]]
+}
+
+example : STHoare p Γ ⟦⟧ (simple_slice.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .bool) => v = false) := by
+  simp only [simple_slice, Expr.mkSlice]
+  steps <;> aesop
+
+nr_def simple_array<>() -> Field {
+  let arr = [1 : Field, 2 : Field];
+  arr[1 : u32]
+}
+
+example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 2) := by
+  simp only [simple_array, Expr.mkArray]
+  steps <;> tauto
+  aesop
diff --git a/Lampe/Lampe/Builtin/Array.lean b/Lampe/Lampe/Builtin/Array.lean
index 896c910..e09f4fd 100644
--- a/Lampe/Lampe/Builtin/Array.lean
+++ b/Lampe/Lampe/Builtin/Array.lean
@@ -1,6 +1,105 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
+lemma _root_.Finmap.insert_mem_disjoint [DecidableEq α] {m₁ m₂ : Finmap fun _ : α => β} {hd : m₁.Disjoint m₂} {he : ref ∈ m₁} :
+  (m₁.insert ref v).Disjoint m₂ := by
+  rw [Finmap.insert_eq_singleton_union]
+  have _ : ref ∉ m₂ := by aesop
+  simp only [Finmap.disjoint_union_left]
+  aesop
+
+lemma Nat.dec_add_eq_self {n : Nat} {h : n ≠ 0} : n - 1 + 1 = n := by
+  cases n
+  contradiction
+  simp
+
+lemma Fin.n_is_non_zero {h : Fin n} : n > 0 := by
+  cases_type Fin
+  cases n
+  contradiction
+  simp
+
+lemma Mathlib.Vector.get_after_erase {idx : Nat} {vec : Mathlib.Vector α n} {h₁ h₂ h₃} :
+  (Mathlib.Vector.eraseIdx ⟨idx, h₁⟩ vec).get ⟨idx, h₂⟩ = Mathlib.Vector.get vec ⟨idx + 1, h₃⟩ := by
+  unfold Mathlib.Vector.get Mathlib.Vector.eraseIdx
+  cases vec
+  simp_all only [Fin.cast_mk, List.get_eq_getElem]
+  rename List _ => l
+  rename_i P
+  subst_vars
+  revert idx
+  induction l
+  . intros
+    rename Nat => idx
+    unfold List.length at *
+    contradiction
+  . rename_i head₁ tail₁ ih
+    intros idx h₁ h₂ h₃
+    cases idx
+    . simp_all
+    . simp only [List.eraseIdx_cons_succ, List.getElem_cons_succ]
+      apply ih
+      . aesop
+      . simp_all only [List.length_cons, add_lt_add_iff_right, add_tsub_cancel_right]
+        rw [←add_lt_add_iff_right (a := 1)]
+        have _ : tail₁.length ≠ 0 := by aesop
+        have ht : tail₁.length - 1 + 1 = tail₁.length := by simp_all [Nat.dec_add_eq_self]
+        simp_all
+      . aesop
+
+lemma Mathlib.Vector.get_after_insert {idx : Nat} {vec : Mathlib.Vector α n} {h} :
+  (Mathlib.Vector.insertNth v ⟨idx, h⟩ vec).get ⟨idx, h⟩ = v := by
+  unfold Mathlib.Vector.insertNth Mathlib.Vector.get
+  cases vec
+  simp_all only [List.get_eq_getElem, Fin.coe_cast]
+  apply List.get_insertNth_self
+  subst_vars
+  linarith
+
+@[reducible]
+def replaceArray' (arr : Tp.denote p (.array tp n)) (idx : Fin n.toNat) (v : Tp.denote p tp) : Tp.denote p (.array tp n) :=
+  let arr' := (arr.insertNth v ⟨idx.val + 1, by aesop⟩)
+  arr'.eraseIdx ⟨idx.val, by cases idx; tauto⟩
+
+example {p} : (replaceArray' (p := p) (n := ⟨3, by aesop⟩) (tp := .bool) ⟨[false, false, false], (by rfl)⟩ ⟨1, by tauto⟩ true).get ⟨1, by tauto⟩ = true := by rfl
+
+@[simp]
+theorem index_replaced_arr {n : U 32} {idx : Fin n.toNat} {arr} :
+  (replaceArray' arr idx v').get idx = v' := by
+  unfold replaceArray'
+  cases em (n.toNat > 0)
+  . simp_all only [gt_iff_lt, eq_mp_eq_cast]
+    generalize h₁ : (Mathlib.Vector.insertNth _ _ _) = arr₁
+    cases idx
+    rw [Mathlib.Vector.get_after_erase, ←h₁]
+    apply Mathlib.Vector.get_after_insert
+  . simp_all only [gt_iff_lt, not_lt, nonpos_iff_eq_zero, lt_self_iff_false, dite_false]
+    rename_i h
+    rw [h] at idx
+    apply Fin.n_is_non_zero at idx
+    contradiction
+
+/--
+Defines the builtin array constructor.
+-/
+def mkArray (n : U 32) := newGenericPureBuiltin
+  (fun (argTps, tp) => ⟨argTps, (.array tp n)⟩)
+  (fun (argTps, tp) args => ⟨argTps = List.replicate n.toNat tp,
+    fun h => HList.toVec args h⟩)
+
+/--
+Defines the indexing of a array `l : Array tp n` with `i : U 32`
+We make the following assumptions:
+- If `i < n`, then the builtin returns `l[i] : Tp.denote tp`
+- Else (out of bounds access), an exception is thrown.
+
+In Noir, this builtin corresponds to `T[i]` for `T: [T; n]` and `i: uint32`.
+-/
+def arrayIndex := newGenericPureBuiltin
+  (fun (tp, n) => ⟨[.array tp n, .u 32], tp⟩)
+  (fun (_, n) h![l, i] => ⟨i.toNat < n.toNat,
+    fun h => l.get (Fin.mk i.toNat h)⟩)
+
 /--
 Defines the function that evaluates to an array's length `n`.
 This builtin evaluates to an `U 32`. Hence, we assume that `n < 2^32`.
@@ -22,4 +121,10 @@ def arrayAsSlice := newGenericPureBuiltin
   (fun (_, _) h![a] => ⟨True,
     fun _ => a.toList⟩)
 
+def replaceArray := newGenericPureBuiltin
+  (fun (tp, n) => ⟨[.array tp n, .u 32, tp], (.array tp n)⟩)
+  (fun (_, n) h![arr, idx, v] => ⟨idx.toNat < n.toNat,
+    fun h => replaceArray' arr ⟨idx.toNat, h⟩ v⟩)
+
+
 end Lampe.Builtin
diff --git a/Lampe/Lampe/Builtin/Slice.lean b/Lampe/Lampe/Builtin/Slice.lean
index 36a9ffa..238da87 100644
--- a/Lampe/Lampe/Builtin/Slice.lean
+++ b/Lampe/Lampe/Builtin/Slice.lean
@@ -1,6 +1,18 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
+@[reducible]
+def replaceSlice' (s : Tp.denote p $ .slice tp) (i : Nat) (v : Tp.denote p tp) : Tp.denote p $ .slice tp :=
+  s.eraseIdx i |>.insertNth i v
+
+/--
+Defines the builtin slice constructor.
+-/
+def mkSlice (n : Nat) := newGenericPureBuiltin
+  (fun (argTps, tp) => ⟨argTps, (.slice tp)⟩)
+  (fun (argTps, tp) args => ⟨argTps = List.replicate n tp,
+    fun h => HList.toList args h⟩)
+
 /--
 Defines the indexing of a slice `l : List tp` with `i : U 32`
 We make the following assumptions:
@@ -105,4 +117,9 @@ def sliceRemove := newGenericPureBuiltin
   (fun _ h![l, i] => ⟨i.toNat < l.length,
     fun h => (l.eraseIdx i.toNat, l.get (Fin.mk i.toNat h), ())⟩)
 
+def replaceSlice := newGenericPureBuiltin
+  (fun tp => ⟨[.slice tp, .u 32, tp], (.slice tp)⟩)
+  (fun _ h![sl, idx, v] => ⟨True,
+    fun _ => replaceSlice' sl idx.toNat v⟩)
+
 end Lampe.Builtin
diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean
index 65521e4..963b7f4 100644
--- a/Lampe/Lampe/Builtin/Struct.lean
+++ b/Lampe/Lampe/Builtin/Struct.lean
@@ -18,13 +18,40 @@ lemma listRep_tp_denote_is_tp_denote_tuple :
     tauto
   }
 
+@[reducible]
+def replaceTuple' (tpl : Tp.denoteArgs p tps) (mem : Member tp tps) (v : Tp.denote p tp) : Tp.denoteArgs p tps := match tps with
+| tp :: _ => match tpl, mem with
+  | (_, rem), .head => (v, rem)
+  | (h, rem), .tail m => (h, replaceTuple' rem m v)
+
+example : replaceTuple' (p := p) exampleTuple Member.head false = (false, 4, 5) := rfl
+example : replaceTuple' (p := p) exampleTuple Member.head.tail 3 = (true, 3, 5) := rfl
+example : replaceTuple' (p := p) exampleTuple Member.head.tail.tail 2 = (true, 4, 2) := rfl
+
+@[simp]
+theorem index_replaced_tpl :
+  indexTpl p (replaceTuple' tpl mem v') mem = v' := by
+  induction mem <;> aesop
+
+/--
+Defines the builtin tuple constructor.
+-/
 def mkTuple := newGenericPureBuiltin
   (fun (name, fieldTps) => ⟨fieldTps, (.tuple name fieldTps)⟩)
   (fun _ fieldExprs => ⟨True,
     fun _ => listRep_tp_denote_is_tp_denote_tuple ▸ HList.toProd fieldExprs⟩)
 
+/--
+Defines the indexing/projection of a tuple with a `Member`.
+-/
 def projectTuple (mem : Member outTp fieldTps) := newGenericPureBuiltin
   (fun name => ⟨[.tuple name fieldTps], outTp⟩)
   (fun _ h![tpl] => ⟨True, fun _ => indexTpl _ tpl mem⟩)
 
+
+def replaceTuple (mem : Member tp tps) := newGenericPureBuiltin
+  (fun name => ⟨[.tuple name tps, tp], (.tuple name tps)⟩)
+  (fun _ h![tpl, v] => ⟨True,
+    fun _ => replaceTuple' tpl mem v⟩)
+
 end Lampe.Builtin
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
index 48a9ac3..cde31bf 100644
--- a/Lampe/Lampe/Hoare/Builtins.lean
+++ b/Lampe/Lampe/Hoare/Builtins.lean
@@ -126,12 +126,25 @@ lemma pureBuiltin_intro_consequence
 
 -- Arrays
 
-theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem mkArray_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} {_ : argTps.length = n} :
+  STHoarePureBuiltin p Γ (Builtin.mkArray n) (by tauto) args (a := (argTps, tp)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
+theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
+theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
+theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
 -- BigInt
@@ -311,6 +324,11 @@ theorem iFromField_intro : STHoarePureBuiltin p Γ Builtin.iFromField (by tauto)
 
 -- Slice
 
+theorem mkSlice_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} {_ : argTps.length = n} :
+  STHoarePureBuiltin p Γ (Builtin.mkSlice n) (by tauto) args (a := (argTps, tp)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
+
 theorem sliceLen_intro : STHoarePureBuiltin p Γ Builtin.sliceLen (by tauto) h![s] := by
   apply pureBuiltin_intro_consequence <;> try rfl
   tauto
@@ -343,6 +361,10 @@ theorem sliceRemove_intro : STHoarePureBuiltin p Γ Builtin.sliceRemove (by taut
   apply pureBuiltin_intro_consequence <;> try rfl
   tauto
 
+theorem replaceSlice_intro : STHoarePureBuiltin p Γ Builtin.replaceSlice (by tauto) h![sl, idx, v] := by
+  apply pureBuiltin_intro_consequence <;> try rfl
+  tauto
+
 -- String
 
 theorem strAsBytes_intro : STHoarePureBuiltin p Γ Builtin.strAsBytes (by tauto) h![s] := by
@@ -451,6 +473,10 @@ theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem)
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
+theorem replaceTuple_intro {mem : Member tp tps} : STHoarePureBuiltin p Γ (Builtin.replaceTuple mem) (by tauto) h![tpl, v] := by
+  apply pureBuiltin_intro_consequence <;> try rfl
+  tauto
+
 -- Misc
 
 theorem assert_intro : STHoarePureBuiltin p Γ Builtin.assert (by tauto) h![a] (a := ()) := by
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
index 2597e47..18f95f1 100644
--- a/Lampe/Lampe/Syntax.lean
+++ b/Lampe/Lampe/Syntax.lean
@@ -34,8 +34,10 @@ partial def mkNrIdent [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [
 
 syntax ident : nr_type
 syntax "${" term "}" : nr_type
-syntax nr_ident "<" nr_type,* ">" : nr_type
-syntax "[" nr_type "]" : nr_type
+syntax nr_ident "<" nr_type,* ">" : nr_type -- Struct
+syntax "[" nr_type "]" : nr_type -- Slice
+syntax "[" nr_type ";" num "]" : nr_type -- Array
+syntax "`(" nr_type,* ")" : nr_type -- Tuple
 
 def mkFieldName (structName : String) (fieldName : String) : Lean.Ident :=
   mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName
@@ -70,11 +72,32 @@ partial def mkNrType [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [M
   `(Struct.tp $(mkStructDefIdent (←mkNrIdent structName)) $(←mkHListLit generics))
 | `(nr_type| ${ $i }) => pure i
 | `(nr_type| [ $tp ]) => do `(Tp.slice $(←mkNrType tp))
+| `(nr_type| [ $tp ; $len:num ]) => do `(Tp.array $(←mkNrType tp) $len)
+| `(nr_type| `($tps,* )) => do
+  let tps ← tps.getElems.toList.mapM mkNrType
+  `(Tp.tuple none $(←mkListLit tps))
 | _ => throwUnsupportedSyntax
 
 def mkBuiltin [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : String) : m (TSyntax `term) :=
    `($(mkIdent $ (Name.mkSimple "Builtin") ++ (Name.mkSimple i)))
 
+@[reducible]
+def typeof {rep : Tp → Type _} (_ : rep tp) := tp
+
+@[reducible]
+def tupleFields (tp : Tp) := match tp with
+| Tp.tuple _ fields => fields
+| _ => []
+
+def mkTupleMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with
+| .zero => `(Member.head)
+| .succ n' => do `(Member.tail $(←mkTupleMember n'))
+
+def mkStructMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) (gs : List $ TSyntax `nr_type) (field : TSyntax `ident) : m (TSyntax `term) := do
+  let gs ← mkHListLit (←gs.mapM fun gVal => mkNrType gVal)
+  let accessor := mkFieldName (←mkNrIdent structName) (field.getId.toString)
+  `($accessor $gs)
+
 syntax ident ":" nr_type : nr_param_decl
 
 syntax num ":" nr_type : nr_expr
@@ -85,7 +108,6 @@ syntax "$" ident : nr_expr
 syntax "let" ident "=" nr_expr : nr_expr
 syntax "let" "mut" ident "=" nr_expr : nr_expr
 syntax ident "=" nr_expr : nr_expr
-syntax nr_expr "." num : nr_expr
 syntax "if" nr_expr nr_expr ("else" nr_expr)? : nr_expr
 syntax "for" ident "in" nr_expr ".." nr_expr nr_expr : nr_expr
 syntax "(" nr_expr ")" : nr_expr
@@ -94,15 +116,21 @@ syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr
 
 syntax nr_typed_expr := nr_expr ":" nr_type
 
-syntax "(" ident "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access
 syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr -- Struct constructor
+syntax "`(" nr_expr,* ")" : nr_expr -- Tuple constructor
+syntax "[" nr_expr,* "]" : nr_expr -- Array constructor
+syntax "&" "[" nr_expr,* "]" : nr_expr -- Slice constructor
+
+syntax "(" nr_expr "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access
+syntax nr_expr "." num ":" nr_type : nr_expr -- Tuple access
+syntax nr_expr "[" nr_expr "]" : nr_expr -- Array access
+syntax nr_expr "[[" nr_expr "]]" : nr_expr -- Slice access
 
 syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Builtin call
 syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr -- Trait call
 syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call
 syntax "@" nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr -- Decl call
 
-
 syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}"
 syntax nr_trait_constraint := nr_type ":" nr_ident "<" nr_type,* ">"
 syntax nr_trait_fn_def := "fn" nr_fn_decl
@@ -110,19 +138,50 @@ syntax nr_trait_impl := "<" ident,* ">" nr_ident "<" nr_type,* ">" "for" nr_type
   "{" sepBy(nr_trait_fn_def, ";", ";", allowTrailingSep) "}"
 syntax nr_struct_def := "<" ident,* ">" "{" sepBy(nr_param_decl, ",", ",", allowTrailingSep) "}"
 
-def Expr.letMutIn (definition : Expr rep tp) (body : rep tp.ref → Expr rep tp'): Expr rep tp' :=
-  let refDef := Expr.letIn definition fun v => Expr.call h![] _ (tp.ref) (.builtin .ref) h![v]
-  Expr.letIn refDef body
-
-def Expr.ref (val : rep tp): Expr rep tp.ref :=
+@[reducible]
+def Expr.ref (val : rep tp) : Expr rep tp.ref :=
   Expr.call h![] _ tp.ref (.builtin .ref) h![val]
 
-def Expr.readRef (ref : rep tp.ref): Expr rep tp :=
+@[reducible]
+def Expr.readRef (ref : rep tp.ref) : Expr rep tp :=
   Expr.call h![] _ tp (.builtin .readRef) h![ref]
 
-def Expr.writeRef (ref : rep tp.ref) (val : rep tp): Expr rep .unit :=
+@[reducible]
+def Expr.writeRef (ref : rep tp.ref) (val : rep tp) : Expr rep .unit :=
   Expr.call h![] _ .unit (.builtin .writeRef) h![ref, val]
 
+@[reducible]
+def Expr.mkSlice (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (.slice tp) :=
+  Expr.call h![] _ (.slice tp) (.builtin $ .mkSlice n) vals
+
+@[reducible]
+def Expr.mkArray (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (.array tp n) :=
+  Expr.call h![] _ (.array tp n) (.builtin $ .mkArray n) vals
+
+@[reducible]
+def Expr.readTuple (tpl : rep $ .tuple name tps) (mem : Member tp tps) : Expr rep tp :=
+  Expr.call h![] [typeof tpl] tp (.builtin (@Builtin.projectTuple tp tps mem)) h![tpl]
+
+@[reducible]
+def Expr.readArray (arr : rep $ .array tp n) (idx : rep $ .u s) : Expr rep tp :=
+  Expr.call h![] _ tp (.builtin .arrayIndex) h![arr, idx]
+
+@[reducible]
+def Expr.readSlice (sl : rep $ .slice tp) (idx : rep $ .u s) : Expr rep tp :=
+  Expr.call h![] _ tp (.builtin .sliceIndex) h![sl, idx]
+
+@[reducible]
+def Expr.replaceTuple (tpl : rep $ .tuple name tps) (mem : Member tp tps) (v : rep tp) : Expr rep (.tuple name tps) :=
+  Expr.call h![] _ (.tuple name tps) (.builtin $ .replaceTuple mem) h![tpl, v]
+
+@[reducible]
+def Expr.replaceArray (arr : rep $ .array tp n) (idx : rep $ .u s) (v : rep tp) : Expr rep (.array tp n) :=
+  Expr.call h![] _ (.array tp n) (.builtin .replaceArray) h![arr, idx, v]
+
+@[reducible]
+def Expr.replaceSlice (sl : rep $ .slice tp) (idx : rep $ .u s) (v : rep tp) : Expr rep (.slice tp) :=
+  Expr.call h![] _ (.slice tp) (.builtin .replaceSlice) h![sl, idx, v]
+
 structure DesugarState where
   autoDeref : Name → Bool
   nextFresh : Nat
@@ -178,35 +237,45 @@ partial def mkArgs [MonadSyntax m] (args : List (TSyntax `nr_expr)) (k : List (T
     mkArgs t fun t => k (h :: t)
 
 partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.Ident) (k : TSyntax `term → m (TSyntax `term)): m (TSyntax `term) := match e with
-| `(nr_expr|$n:num : $tp) => do wrapSimple (←`(Lampe.Expr.lit $(←mkNrType tp) $n)) vname k
-| `(nr_expr| true) => do wrapSimple (←`(Lampe.Expr.lit Tp.bool 1)) vname k
-| `(nr_expr| false) => do wrapSimple (←`(Lampe.Expr.lit Tp.bool 0)) vname k
+| `(nr_expr|$n:num : $tp) => do wrapSimple (←`(Expr.lit $(←mkNrType tp) $n)) vname k
+| `(nr_expr| true) => do wrapSimple (←`(Expr.lit Tp.bool 1)) vname k
+| `(nr_expr| false) => do wrapSimple (←`(Expr.lit Tp.bool 0)) vname k
 | `(nr_expr| { $exprs;* }) => mkBlock exprs.getElems.toList k
 | `(nr_expr| $i:ident) => do
-  if ←isAutoDeref i.getId then wrapSimple (← `(Lampe.Expr.readRef $i)) vname k else match vname with
+  if ←isAutoDeref i.getId then wrapSimple (← `(Expr.readRef $i)) vname k else match vname with
   | none => k i
-  | some _ => wrapSimple (←`(Lampe.Expr.var $i)) vname k
+  | some _ => wrapSimple (←`(Expr.var $i)) vname k
 | `(nr_expr| # $i:ident ($args,*): $tp) => do
   mkArgs args.getElems.toList fun argVals => do
-    wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.builtin $(←mkBuiltin i.getId.toString)) $(←mkHListLit argVals))) vname k
+    wrapSimple (←`(Expr.call h![] _ $(←mkNrType tp) (.builtin $(←mkBuiltin i.getId.toString)) $(←mkHListLit argVals))) vname k
 | `(nr_expr| for $i in $lo .. $hi $body) => do
   mkExpr lo none fun lo =>
   mkExpr hi none fun hi => do
-    let body ← mkExpr body none (fun x => `(Lampe.Expr.var $x))
-    wrapSimple (←`(Lampe.Expr.loop $lo $hi fun $i => $body)) vname k
+    let body ← mkExpr body none (fun x => `(Expr.var $x))
+    wrapSimple (←`(Expr.loop $lo $hi fun $i => $body)) vname k
 | `(nr_expr| $v:ident = $e) => do
   mkExpr e none fun eVal => do
-    wrapSimple (←`(Lampe.Expr.writeRef $v $eVal)) vname k
+    wrapSimple (←`(Expr.writeRef $v $eVal)) vname k
 | `(nr_expr| ( $e )) => mkExpr e vname k
 | `(nr_expr| if $cond $mainBody else $elseBody) => do
     mkExpr cond none fun cond => do
-      let mainBody ← mkExpr mainBody none fun x => `(Lampe.Expr.var $x)
-      let elseBody ← mkExpr elseBody none fun x => `(Lampe.Expr.var $x)
-      wrapSimple (←`(Lampe.Expr.ite $cond $mainBody $elseBody)) vname k
+      let mainBody ← mkExpr mainBody none fun x => `(Expr.var $x)
+      let elseBody ← mkExpr elseBody none fun x => `(Expr.var $x)
+      wrapSimple (←`(Expr.ite $cond $mainBody $elseBody)) vname k
 | `(nr_expr| if $cond $mainBody) => do
     mkExpr cond none fun cond => do
-      let mainBody ← mkExpr mainBody none fun x => `(Lampe.Expr.var $x)
-      wrapSimple (←`(Lampe.Expr.ite $cond $mainBody (Lampe.Expr.skip))) vname k
+      let mainBody ← mkExpr mainBody none fun x => `(Expr.var $x)
+      wrapSimple (←`(Expr.ite $cond $mainBody (Expr.skip))) vname k
+| `(nr_expr| & [ $args,* ]) => do
+  let args := args.getElems.toList
+  let len := args.length
+  mkArgs args fun argVals => do
+    wrapSimple (←`(Expr.mkSlice $(Syntax.mkNumLit $ toString len) $(←mkHListLit argVals))) vname k
+| `(nr_expr| [ $args,* ]) => do
+  let args := args.getElems.toList
+  let len := args.length
+  mkArgs args fun argVals => do
+    wrapSimple (←`(Expr.mkArray $(Syntax.mkNumLit $ toString len) $(←mkHListLit argVals))) vname k
 | `(nr_expr| | $params,* | -> $outTp $lambdaBody) => do
   let outTp ← mkNrType outTp
   let argTps ← mkListLit (← params.getElems.toList.mapM fun param => match param with
@@ -215,16 +284,16 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
   let args ← mkHListLit (← params.getElems.toList.mapM fun param => match param with
     | `(nr_param_decl|$i:ident : $_) => `($i)
     | _ => throwUnsupportedSyntax)
-  let body ← mkExpr lambdaBody none fun x => `(Lampe.Expr.var $x)
-  wrapSimple (←`(Lampe.Expr.lambda $argTps $outTp (fun $args => $body))) vname k
+  let body ← mkExpr lambdaBody none fun x => `(Expr.var $x)
+  wrapSimple (←`(Expr.lambda $argTps $outTp (fun $args => $body))) vname k
 | `(nr_expr| ^ $i:ident ($args,*) : $tp) => do
   mkArgs args.getElems.toList fun argVals => do
-    wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k
+    wrapSimple (←`(Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k
 | `(nr_expr| @ $declName:nr_ident < $callGenVals:nr_type,* > ( $args,* ) : $tp) => do
    let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type))
    let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
    mkArgs args.getElems.toList fun argVals => do
-     wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k
+     wrapSimple (←`(@Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k
 | `(nr_expr| ( $selfTp as $traitName < $traitGenVals,* > ) :: $methodName < $callGenVals,* > ( $args,* ) : $tp) => do
   let argTps ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $_ : $ty) => mkNrType ty | _ => throwUnsupportedSyntax
   let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax
@@ -235,19 +304,34 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
   let methodName ← mkNrIdent methodName
   let traitName ← mkNrIdent traitName
   mkArgs argExprs fun argVals => do
-    wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals $(←mkListLit argTps) $(←mkNrType tp)
+    wrapSimple (←`(@Expr.call _ $callGenKinds $callGenVals $(←mkListLit argTps) $(←mkNrType tp)
       (.trait ⟨⟨⟨$(Syntax.mkStrLit traitName), $traitGenKinds, $traitGenVals⟩, $(←mkNrType selfTp)⟩, $(Syntax.mkStrLit methodName)⟩) $(←mkHListLit argVals))) vname k
 | `(nr_expr| $structName:nr_ident < $structGenVals,* > { $args,* }) => do
    let structGenValsSyn ← mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
    let paramTpsSyn ← `(Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) $structGenValsSyn)
    let structName ← mkNrIdent structName
    mkArgs args.getElems.toList fun argVals => do
-     wrapSimple (←`(Lampe.Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $paramTpsSyn) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k
-| `(nr_expr| ( $ref:ident as $structName:nr_ident  < $structGenVals,* > ) . $structField:ident) => do
-  let structGenValsSyn ← mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
-  let accessor := mkFieldName (←mkNrIdent structName) (structField.getId.toString)
-  let accessorSyn ← `($accessor $structGenValsSyn)
-  `(.call h![] [.tuple _ _] _ (.builtin (.projectTuple $accessorSyn)) h![$ref])
+     wrapSimple (←`(Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $paramTpsSyn) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k
+| `(nr_expr| `( $args,* )) => do
+  mkArgs args.getElems.toList fun argVals => do
+    let argTps ← argVals.mapM fun arg => `(typeof $arg)
+    wrapSimple (←`(Expr.call h![] _ (.tuple none $(←mkListLit argTps)) (.builtin Builtin.mkTuple) $(←mkHListLit argVals))) vname k
+| `(nr_expr| ( $lhsExpr:nr_expr as $structName:nr_ident  < $structGenVals,* > ) . $structField:ident) => do
+  let mem ← mkStructMember structName structGenVals.getElems.toList structField
+  mkExpr lhsExpr none fun tpl => do
+    wrapSimple (←`(Expr.readTuple $tpl $mem)) vname k
+| `(nr_expr| $tupleExpr:nr_expr . $idx:num : $_:nr_type) => do
+  let mem ← mkTupleMember idx.getNat
+  mkExpr tupleExpr none fun tpl => do
+    wrapSimple (←`(Expr.readTuple $tpl $mem)) vname k
+| `(nr_expr| $lhsExpr:nr_expr [ $idxExpr:nr_expr ]) => do
+  mkExpr idxExpr none fun idx => do
+    mkExpr lhsExpr none fun arr => do
+      wrapSimple (←`(Expr.readArray $arr $idx)) vname k
+| `(nr_expr| $lhsExpr:nr_expr [[ $idxExpr:nr_expr ]]) => do
+  mkExpr idxExpr none fun idx => do
+    mkExpr lhsExpr none fun arr => do
+      wrapSimple (←`(Expr.readSlice $arr $idx)) vname k
 | _ => throwUnsupportedSyntax
 
 end
@@ -311,10 +395,6 @@ def mkStructDef [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadE
   pure syn
 | _ => throwUnsupportedSyntax
 
-def mkTplMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with
-| .zero => `(Member.head)
-| .succ n' => do `(Member.tail $(←mkTplMember n'))
-
 def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) : Syntax → m (List $ TSyntax `command)
 | `(nr_struct_def| < $generics,* > { $params,* }) => do
   let genericKinds ← mkListLit (←generics.getElems.toList.mapM fun _ => `(Kind.type))
@@ -324,7 +404,7 @@ def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [
       let paramDefTy ← `(match generics with
         | $(←mkHListLit generics) => Member $(←mkNrType paramType) (Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) generics))
       let paramDefSyn ← `(match generics with
-        | $(←mkHListLit generics) => $(←mkTplMember idx))
+        | $(←mkHListLit generics) => $(←mkTupleMember idx))
       let defnNameSyn := mkFieldName (←mkNrIdent structName) paramName.getId.toString
       `(def $defnNameSyn (generics : HList Kind.denote $genericKinds) : $paramDefTy := $paramDefSyn)
     | _ => throwUnsupportedSyntax
diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
index db7531f..d755210 100644
--- a/Lampe/Lampe/Tactic/SeparationLogic.lean
+++ b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -60,7 +60,6 @@ theorem exists_star [LawfulHeap α] {P : SLP α} {Q : β → SLP α} : ((∃∃x
   simp [SLP.star_comm]
 
 theorem Lampe.STHoare.litU_intro: STHoare p Γ ⟦⟧ (.lit (.u s) n) fun v => v = n := by
-  -- apply litU_intro
   unfold STHoare THoare
   intro H st hp
   constructor
@@ -68,6 +67,31 @@ theorem Lampe.STHoare.litU_intro: STHoare p Γ ⟦⟧ (.lit (.u s) n) fun v => v
   apply SLP.ent_star_top
   assumption
 
+theorem Lampe.STHoare.litField_intro: STHoare p Γ ⟦⟧ (.lit .field n) fun v => v = n := by
+  unfold STHoare THoare
+  intro H st hp
+  constructor
+  simp only
+  apply SLP.ent_star_top
+  assumption
+
+theorem Lampe.STHoare.litFalse_intro: STHoare p Γ ⟦⟧ (.lit .bool 0) fun v => v = false := by
+  unfold STHoare THoare
+  intro H st hp
+  constructor
+  simp only
+  apply SLP.ent_star_top
+  assumption
+
+theorem Lampe.STHoare.litTrue_intro: STHoare p Γ ⟦⟧ (.lit .bool 1) fun v => v = true := by
+  unfold STHoare THoare
+  intro H st hp
+  constructor
+  simp only
+  apply SLP.ent_star_top
+  assumption
+
+
 theorem ref_intro' {p} {x : Tp.denote p tp} {Γ P}:
     STHoare p Γ P (.ref x) fun v => [v ↦ ⟨tp, x⟩] ⋆ P := by
   apply ramified_frame_top
@@ -531,6 +555,9 @@ elab "sl" : tactic => do
 macro "stephelper1" : tactic => `(tactic|(
   (first
     | apply Lampe.STHoare.litU_intro
+    | apply Lampe.STHoare.litField_intro
+    | apply Lampe.STHoare.litTrue_intro
+    | apply Lampe.STHoare.litFalse_intro
     | apply fresh_intro
     | apply assert_intro
     | apply skip_intro
@@ -539,15 +566,23 @@ macro "stephelper1" : tactic => `(tactic|(
     | apply cast_intro
     | apply callTrait_intro
     | apply callDecl_intro
-    -- memory builtins
+    -- memory
     | apply var_intro
     | apply ref_intro
     | apply readRef_intro
     | apply writeRef_intro
-    -- slice builtins
+    -- array
+    | apply mkArray_intro
+    | apply arrayLen_intro
+    | apply arrayIndex_intro
+    | apply arrayAsSlice_intro
+    | apply replaceArray_intro
+    -- slice
+    | apply mkSlice_intro
     | apply sliceLen_intro
     | apply sliceIndex_intro
     | apply slicePushBack_intro
+    | apply replaceSlice_intro
     -- equality
     | apply unitEq_intro
     | apply bEq_intro
@@ -585,25 +620,37 @@ macro "stephelper1" : tactic => `(tactic|(
     -- struct
     | apply mkTuple_intro
     | apply projectTuple_intro
+    | apply replaceTuple_intro
   )
 ))
 
 macro "stephelper2" : tactic => `(tactic|(
   (first
-    | apply consequence_frame_left fresh_intro
     | apply consequence_frame_left Lampe.STHoare.litU_intro
+    | apply consequence_frame_left Lampe.STHoare.litField_intro
+    | apply consequence_frame_left Lampe.STHoare.litTrue_intro
+    | apply consequence_frame_left Lampe.STHoare.litFalse_intro
+    | apply consequence_frame_left fresh_intro
     | apply consequence_frame_left assert_intro
     | apply consequence_frame_left lam_intro
     | apply consequence_frame_left cast_intro
-    -- memory builtins
+    -- memory
     | apply consequence_frame_left var_intro
     | apply consequence_frame_left ref_intro
     | apply consequence_frame_left readRef_intro
     | apply consequence_frame_left writeRef_intro
-    -- slice builtins
+    -- array
+    | apply consequence_frame_left mkArray_intro
+    | apply consequence_frame_left arrayLen_intro
+    | apply consequence_frame_left arrayIndex_intro
+    | apply consequence_frame_left arrayAsSlice_intro
+    | apply consequence_frame_left replaceArray_intro
+    -- slice
+    | apply consequence_frame_left mkSlice_intro
     | apply consequence_frame_left sliceLen_intro
     | apply consequence_frame_left sliceIndex_intro
     | apply consequence_frame_left slicePushBack_intro
+    | apply consequence_frame_left replaceSlice_intro
     -- equality
     | apply consequence_frame_left unitEq_intro
     | apply consequence_frame_left bEq_intro
@@ -641,28 +688,40 @@ macro "stephelper2" : tactic => `(tactic|(
     -- struct
     | apply consequence_frame_left mkTuple_intro
     | apply consequence_frame_left projectTuple_intro
+    | apply consequence_frame_left replaceTuple_intro
   )
   repeat sl
 ))
 
 macro "stephelper3" : tactic => `(tactic|(
   (first
-    | apply ramified_frame_top fresh_intro
     | apply ramified_frame_top Lampe.STHoare.litU_intro
+    | apply ramified_frame_top Lampe.STHoare.litField_intro
+    | apply ramified_frame_top Lampe.STHoare.litTrue_intro
+    | apply ramified_frame_top Lampe.STHoare.litFalse_intro
+    | apply ramified_frame_top fresh_intro
     | apply ramified_frame_top assert_intro
     | apply ramified_frame_top skip_intro
     | apply ramified_frame_top lam_intro
     | apply ramified_frame_top cast_intro
     | apply ramified_frame_top callDecl_intro
-    -- memory builtins
+    -- memory
     | apply ramified_frame_top var_intro
     | apply ramified_frame_top ref_intro
     | apply ramified_frame_top readRef_intro
     | apply ramified_frame_top writeRef_intro
-    -- slice builtins
+    -- array
+    | apply ramified_frame_top mkArray_intro
+    | apply ramified_frame_top arrayLen_intro
+    | apply ramified_frame_top arrayIndex_intro
+    | apply ramified_frame_top arrayAsSlice_intro
+    | apply ramified_frame_top replaceArray_intro
+    -- slice
+    | apply ramified_frame_top mkSlice_intro
     | apply ramified_frame_top sliceLen_intro
     | apply ramified_frame_top sliceIndex_intro
     | apply ramified_frame_top slicePushBack_intro
+    | apply ramified_frame_top replaceSlice_intro
     -- equality
     | apply ramified_frame_top unitEq_intro
     | apply ramified_frame_top bEq_intro
@@ -700,6 +759,7 @@ macro "stephelper3" : tactic => `(tactic|(
     -- struct
     | apply ramified_frame_top mkTuple_intro
     | apply ramified_frame_top projectTuple_intro
+    | apply ramified_frame_top replaceTuple_intro
   )
   repeat sl
 ))
diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean
index 114f71d..4ac72c8 100644
--- a/Lampe/Lampe/Tp.lean
+++ b/Lampe/Lampe/Tp.lean
@@ -82,4 +82,38 @@ example : newMember [.bool, .field, .field] ⟨0, (by tauto)⟩ = Member.head :=
 example : newMember [.bool, .field, .field] ⟨1, (by tauto)⟩ = Member.head.tail := rfl
 example : newMember [.bool, .field, .field] ⟨2, (by tauto)⟩ = Member.head.tail.tail := rfl
 
+lemma List.replicate_head (hl : x :: xs = List.replicate n a) : x = a := by
+  unfold List.replicate at hl
+  aesop
+
+lemma List.replicate_cons (hl : x :: xs = List.replicate n a) : xs = List.replicate (n-1) a := by
+  unfold List.replicate at hl
+  cases xs <;> aesop
+
+@[reducible]
+def HList.toList (l : HList rep tps) (_ : tps = List.replicate n tp) : List (rep tp) := match l with
+| .nil => []
+| .cons x xs => match tps with
+  | [] => []
+  | _ :: _ => ((List.replicate_head (by tauto)) ▸ x) :: (HList.toList xs (List.replicate_cons (by tauto)))
+
+lemma HList.toList_cons :
+  HList.toList (n := n + 1) (HList.cons head rem) h₁ = head :: (HList.toList (n := n) rem h₂) := by
+  rfl
+
+lemma HList.toList_length_is_n (h_same : tps = List.replicate n tp) :
+  (HList.toList l h_same).length = n := by
+  subst h_same
+  induction n
+  cases l
+  tauto
+  cases l
+  rw [HList.toList_cons]
+  simp_all
+  rfl
+
+@[reducible]
+def HList.toVec (l : HList rep tps) (h_same : tps = List.replicate n tp) : Mathlib.Vector (rep tp) n :=
+  ⟨HList.toList l h_same, by apply HList.toList_length_is_n⟩
+
 end Lampe