diff --git a/Clean/Circuit/Basic.lean b/Clean/Circuit/Basic.lean
index 03d5087..b39f187 100644
--- a/Clean/Circuit/Basic.lean
+++ b/Clean/Circuit/Basic.lean
@@ -1,7 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
 import Clean.Circuit.Expression
 import Clean.Circuit.Provable
 
@@ -197,7 +193,7 @@ def assign_cell (c: Cell F) (v: Variable F) := as_circuit (
 -- formal concepts of soundness and completeness of a circuit
 
 @[simp]
-def constraints_hold_from_list [Field F] (env: (ℕ → F)) : List (Operation F) → Prop
+def constraints_hold_from_list (env: (ℕ → F)) : List (Operation F) → Prop
   | [] => True
   | op :: [] => match op with
     | Operation.Assert e => (e.eval_env env) = 0
@@ -213,7 +209,7 @@ def constraints_hold_from_list [Field F] (env: (ℕ → F)) : List (Operation F)
     | _ => constraints_hold_from_list env ops
 
 @[reducible, simp]
-def constraints_hold [Field F] (env: (ℕ → F)) (circuit: Circuit F α) (ctx : Context F := .empty) : Prop :=
+def constraints_hold (env: (ℕ → F)) (circuit: Circuit F α) (ctx : Context F := .empty) : Prop :=
   constraints_hold_from_list env (circuit ctx).1.2
 
 /--
@@ -223,7 +219,7 @@ witness generator, checking all constraints would not fail.
 For subcircuits, since we proved completeness, this only means we need to satisfy the assumptions!
 -/
 @[simp]
-def constraints_hold_from_list_default [Field F] : List (Operation F) → Prop
+def constraints_hold_from_list_default : List (Operation F) → Prop
   | [] => True
   | op :: [] => match op with
     | Operation.Assert e => e.eval = 0
diff --git a/Clean/Circuit/Expression.lean b/Clean/Circuit/Expression.lean
index 4f18db9..68cebef 100644
--- a/Clean/Circuit/Expression.lean
+++ b/Clean/Circuit/Expression.lean
@@ -1,7 +1,4 @@
 import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
 
 variable {F: Type}
 
diff --git a/Clean/Circuit/Provable.lean b/Clean/Circuit/Provable.lean
index 3ce35dd..a97cd66 100644
--- a/Clean/Circuit/Provable.lean
+++ b/Clean/Circuit/Provable.lean
@@ -1,6 +1,4 @@
-import Mathlib.Algebra.Field.Basic
 import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
 import Clean.Utils.Vector
 import Clean.Circuit.Expression
 
diff --git a/Clean/Circuit/SubCircuit.lean b/Clean/Circuit/SubCircuit.lean
index af669d9..8e1d1df 100644
--- a/Clean/Circuit/SubCircuit.lean
+++ b/Clean/Circuit/SubCircuit.lean
@@ -3,59 +3,147 @@ import Clean.Circuit.Basic
 variable {F: Type} [Field F]
 
 namespace PreOperation
--- in the following, we prove equivalence between flattened and nested constraints
 
 def to_flat_operations [Field F] (ops: List (Operation F)) : List (PreOperation F) :=
   match ops with
   | [] => []
   | op :: ops => match op with
-    | Operation.Witness compute => PreOperation.Witness compute :: to_flat_operations ops
-    | Operation.Assert e => PreOperation.Assert e :: to_flat_operations ops
-    | Operation.Lookup l => PreOperation.Lookup l :: to_flat_operations ops
-    | Operation.Assign (c, v) => PreOperation.Assign (c, v) :: to_flat_operations ops
+    | Operation.Witness c => Witness c :: to_flat_operations ops
+    | Operation.Assert e => Assert e :: to_flat_operations ops
+    | Operation.Lookup l => Lookup l :: to_flat_operations ops
+    | Operation.Assign c => Assign c :: to_flat_operations ops
     | Operation.SubCircuit circuit => circuit.ops ++ to_flat_operations ops
 
--- TODO super painful, mainly because `cases` doesn't allow rich patterns -- how does this work again?
-theorem can_flatten_first : ∀ (env: ℕ → F) (ops: List (Operation F)),
-  PreOperation.constraints_hold env (to_flat_operations ops)
-  → Circuit.constraints_hold_from_list env ops
+open Circuit (constraints_hold_from_list constraints_hold_from_list_default)
+
+lemma constraints_hold_cons : ∀ {op : PreOperation F}, ∀ {ops: List (PreOperation F)}, ∀ {env : ℕ → F},
+  constraints_hold env (op :: ops) ↔ constraints_hold env [op] ∧ constraints_hold env ops := by
+  intro op ops env
+  match ops with
+  | [] => tauto
+  | op' :: ops =>
+    constructor <;> (
+      rintro h
+      dsimp only [constraints_hold] at h
+      split at h
+      <;> simp_all only [constraints_hold, and_self])
+
+lemma constraints_hold_append : ∀ {a b: List (PreOperation F)}, ∀ {env : ℕ → F},
+  constraints_hold env (a ++ b) ↔ constraints_hold env a ∧ constraints_hold env b := by
+  intro a b env
+  induction a with
+  | nil => rw [List.nil_append]; tauto
+  | cons op ops ih =>
+    constructor
+    · intro h
+      rw [List.cons_append] at h
+      obtain ⟨ h_op, h_rest ⟩ := constraints_hold_cons.mp h
+      obtain ⟨ h_ops, h_b ⟩ := ih.mp h_rest
+      exact ⟨ constraints_hold_cons.mpr ⟨ h_op, h_ops ⟩, h_b ⟩
+    · rintro ⟨ h_a, h_b ⟩
+      obtain ⟨ h_op, h_ops ⟩ := constraints_hold_cons.mp h_a
+      have h_rest := ih.mpr ⟨ h_ops, h_b ⟩
+      exact constraints_hold_cons.mpr ⟨ h_op, h_rest ⟩
+
+/--
+Main soundness theorem which proves that flattened constraints imply nested constraints.
+
+It thereby justifies relying on the nested version `Circuit.constraints_hold_from_list`,
+where constraints of subcircuits are replaced with higher-level statements
+that imply (or are implied by) those constraints.
+-/
+theorem can_replace_subcircuits : ∀ {ops: List (Operation F)}, ∀ {env : ℕ → F},
+  constraints_hold env (to_flat_operations ops) → constraints_hold_from_list env ops
 := by
-  intro env ops
-  induction ops with
-  | nil => intro h; exact h
+  intro ops env h
+  -- `to_flat_operations.induct` (functional induction for `to_flat_operations`) is matching on
+  -- empty vs non-empty lists, and different cases for the head in the non-empty case, at the same time.
+  induction ops using to_flat_operations.induct with
+  | case1 => tauto
+  -- we can handle all non-empty cases except `SubCircuit` at once
+  | case2 ops _ ih | case3 ops _ ih | case4 ops _ ih | case5 ops _ ih =>
+    dsimp only [to_flat_operations] at h
+    generalize to_flat_operations ops = flatops at h ih
+    cases ops
+    <;> cases flatops
+    <;> try dsimp only [constraints_hold, constraints_hold_from_list] at h; tauto
+  | case6 ops circuit ih =>
+    dsimp only [to_flat_operations] at h
+    have h_subcircuit : constraints_hold env circuit.ops := (constraints_hold_append.mp h).left
+    have h_rest : constraints_hold env (to_flat_operations ops) := (constraints_hold_append.mp h).right
+    cases ops
+    <;> dsimp only [constraints_hold_from_list]
+    <;> use (circuit.imply_soundness env) h_subcircuit
+    use ih h_rest
+
+-- TODO the following two lemmas would be unnecessary if we could prove `constraints_hold_default` to be a special case of `constraints_hold`
+-- see https://github.com/Verified-zkEVM/clean/issues/42
+
+lemma constraints_hold_default_cons : ∀ {op : PreOperation F}, ∀ {ops: List (PreOperation F)},
+  constraints_hold_default (op :: ops) ↔ constraints_hold_default [op] ∧ constraints_hold_default ops := by
+  intro op ops
+  match ops with
+  | [] => tauto
+  | op' :: ops =>
+    constructor <;> (
+      rintro h
+      dsimp only [constraints_hold_default] at h
+      split at h
+      <;> simp_all only [constraints_hold_default, and_self])
+
+lemma constraints_hold_default_append : ∀ {a b: List (PreOperation F)},
+  constraints_hold_default (a ++ b) ↔ constraints_hold_default a ∧ constraints_hold_default b := by
+  intro a b
+  induction a with
+  | nil => rw [List.nil_append]; tauto
   | cons op ops ih =>
-    cases ops with
-    | nil =>
-      simp at ih
-      cases op with
-      | SubCircuit c =>
-        sorry
-      | _ => simp [PreOperation.constraints_hold]
-    | cons op' ops' =>
-      let ops := op' :: ops'
-      cases op with
-      | SubCircuit c => sorry
-      | Assert e => sorry
-      | Witness c =>
-        have h_ops : to_flat_operations (Operation.Witness c :: op' :: ops') = PreOperation.Witness c :: to_flat_operations (op' :: ops') := rfl
-        rw [h_ops]
-        intro h_pre
-        have h1 : PreOperation.constraints_hold env (to_flat_operations (op' :: ops')) := by
-          rw [PreOperation.constraints_hold] at h_pre
-          · exact h_pre
-          · sorry
-          · simp
-          · simp
-        have ih1 := ih h1
-        simp [ih1]
-      | Lookup l => sorry
-      | Assign a => sorry
-
-theorem can_flatten : ∀ (ops: List (Operation F)),
-  Circuit.constraints_hold_from_list_default ops →
-  PreOperation.constraints_hold_default (to_flat_operations ops)
+    constructor
+    · intro h
+      rw [List.cons_append] at h
+      obtain ⟨ h_op, h_rest ⟩ := constraints_hold_default_cons.mp h
+      obtain ⟨ h_ops, h_b ⟩ := ih.mp h_rest
+      exact ⟨ constraints_hold_default_cons.mpr ⟨ h_op, h_ops ⟩, h_b ⟩
+    · rintro ⟨ h_a, h_b ⟩
+      obtain ⟨ h_op, h_ops ⟩ := constraints_hold_default_cons.mp h_a
+      have h_rest := ih.mpr ⟨ h_ops, h_b ⟩
+      exact constraints_hold_default_cons.mpr ⟨ h_op, h_rest ⟩
+
+/--
+Main completeness theorem which proves that nested constraints imply flattened constraints
+using the default witness generator.
+
+This justifies only proving the nested version `Circuit.constraints_hold_from_list_default`,
+where constraints of subcircuits are replaced with higher-level statements
+that imply (or are implied by) those constraints.
+
+Note: Ideally, `can_replace_subcircuits` would prove both directions, and this would be just a special
+case. See https://github.com/Verified-zkEVM/clean/issues/42
+-/
+theorem can_replace_subcircuits_default : ∀ {ops: List (Operation F)},
+  constraints_hold_from_list_default ops → constraints_hold_default (to_flat_operations ops)
 := by
- sorry
+  intro ops h
+  -- `to_flat_operations.induct` (functional induction for `to_flat_operations`) is matching on
+  -- empty vs non-empty lists, and different cases for the head in the non-empty case, at the same time.
+  induction ops using to_flat_operations.induct with
+  | case1 => tauto
+  -- we can handle all non-empty cases except `SubCircuit` at once
+  | case2 ops _ ih | case3 ops _ ih | case4 ops _ ih | case5 ops _ ih =>
+    dsimp only [to_flat_operations]
+    generalize to_flat_operations ops = flatops at *
+    cases ops
+    <;> dsimp only [constraints_hold_from_list_default] at h
+    <;> cases flatops
+    <;> dsimp only [constraints_hold_default]
+    <;> tauto
+  | case6 ops circuit ih =>
+    dsimp only [to_flat_operations]
+    apply constraints_hold_default_append.mpr
+    cases ops
+    · use circuit.implied_by_completeness h; tauto
+    dsimp only [constraints_hold_from_list_default] at h
+    exact ⟨ circuit.implied_by_completeness h.left, ih h.right ⟩
+
 end PreOperation
 
 variable {α β: TypePair} [ProvableType F α] [ProvableType F β]
@@ -91,7 +179,7 @@ def formal_circuit_to_subcircuit (ctx: Context F)
 
     -- so we just need to go from flattened constraints to constraints
     guard_hyp h_holds : PreOperation.constraints_hold env (PreOperation.to_flat_operations ops)
-    exact PreOperation.can_flatten_first env ops h_holds
+    exact PreOperation.can_replace_subcircuits h_holds
 
     -- `implied_by_completeness`
     -- we are given that the assumptions are true
@@ -103,7 +191,7 @@ def formal_circuit_to_subcircuit (ctx: Context F)
     have h_holds : constraints_hold_from_list_default ops := circuit.completeness ctx b b_var rfl as
 
     -- so we just need to go from constraints to flattened constraints
-    exact PreOperation.can_flatten ops h_holds
+    exact PreOperation.can_replace_subcircuits_default h_holds
 
   ⟨ a_var, s ⟩
 
@@ -133,7 +221,7 @@ def formal_assertion_to_subcircuit (ctx: Context F)
 
     -- so we just need to go from flattened constraints to constraints
     guard_hyp h_holds : PreOperation.constraints_hold env (PreOperation.to_flat_operations ops)
-    exact PreOperation.can_flatten_first env ops h_holds
+    exact PreOperation.can_replace_subcircuits h_holds
 
     -- `implied_by_completeness`
     -- we are given that the assumptions and the spec are true
@@ -145,7 +233,7 @@ def formal_assertion_to_subcircuit (ctx: Context F)
     have h_holds : constraints_hold_from_list_default ops := circuit.completeness ctx b b_var rfl as.left as.right
 
     -- so we just need to go from constraints to flattened constraints
-    exact PreOperation.can_flatten ops h_holds
+    exact PreOperation.can_replace_subcircuits_default h_holds
 
   s
 end Circuit
diff --git a/Clean/Examples/Gadgets.lean b/Clean/Examples/Gadgets.lean
index 0e07c58..4ca87b0 100644
--- a/Clean/Examples/Gadgets.lean
+++ b/Clean/Examples/Gadgets.lean
@@ -1,15 +1,9 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
 import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
 import Clean.GadgetsNew.Add8.Addition8
 
 section
 
-#eval!
+#eval
   let p := 1009
   let p_prime := Fact.mk prime_1009
   let p_non_zero := Fact.mk (by norm_num : p ≠ 0)
diff --git a/Clean/GadgetsNew/Add8/Addition8.lean b/Clean/GadgetsNew/Add8/Addition8.lean
index 1bd2e7a..2edf1d5 100644
--- a/Clean/GadgetsNew/Add8/Addition8.lean
+++ b/Clean/GadgetsNew/Add8/Addition8.lean
@@ -1,13 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Utils.Field
-import Clean.GadgetsNew.ByteLookup
-import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Addition8Full
 
 namespace Add8
diff --git a/Clean/GadgetsNew/Add8/Addition8Full.lean b/Clean/GadgetsNew/Add8/Addition8Full.lean
index 3274c4e..7c1342d 100644
--- a/Clean/GadgetsNew/Add8/Addition8Full.lean
+++ b/Clean/GadgetsNew/Add8/Addition8Full.lean
@@ -1,14 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Circuit.SubCircuit
-import Clean.Utils.Field
-import Clean.GadgetsNew.ByteLookup
-import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Addition8FullCarry
 
 namespace Add8Full
diff --git a/Clean/GadgetsNew/Add8/Addition8FullCarry.lean b/Clean/GadgetsNew/Add8/Addition8FullCarry.lean
index 9722480..a8a8fdf 100644
--- a/Clean/GadgetsNew/Add8/Addition8FullCarry.lean
+++ b/Clean/GadgetsNew/Add8/Addition8FullCarry.lean
@@ -1,12 +1,4 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
 import Clean.Circuit.SubCircuit
-import Clean.Utils.Field
 import Clean.GadgetsNew.ByteLookup
 import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Theorems
diff --git a/Clean/GadgetsNew/Add8/Theorems.lean b/Clean/GadgetsNew/Add8/Theorems.lean
index cc1f2d9..2a8b857 100644
--- a/Clean/GadgetsNew/Add8/Theorems.lean
+++ b/Clean/GadgetsNew/Add8/Theorems.lean
@@ -1,10 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
 import Clean.Utils.Field
 
 namespace Add8Theorems
diff --git a/Clean/GadgetsNew/Addition32Full.lean b/Clean/GadgetsNew/Addition32Full.lean
index f8b7459..6a805b2 100644
--- a/Clean/GadgetsNew/Addition32Full.lean
+++ b/Clean/GadgetsNew/Addition32Full.lean
@@ -1,14 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Circuit.SubCircuit
-import Clean.Utils.Field
-import Clean.GadgetsNew.ByteLookup
-import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Addition8FullCarry
 import Clean.Types.U32
 
diff --git a/Clean/GadgetsNew/Boolean.lean b/Clean/GadgetsNew/Boolean.lean
index 32d4ab2..317cbde 100644
--- a/Clean/GadgetsNew/Boolean.lean
+++ b/Clean/GadgetsNew/Boolean.lean
@@ -1,9 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
 import Clean.Circuit.Basic
 import Clean.Utils.Field
 
diff --git a/Clean/GadgetsNew/ByteLookup.lean b/Clean/GadgetsNew/ByteLookup.lean
index da8db7f..8794c09 100644
--- a/Clean/GadgetsNew/ByteLookup.lean
+++ b/Clean/GadgetsNew/ByteLookup.lean
@@ -1,9 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
 import Clean.Circuit.Basic
 import Clean.Utils.Field
 
@@ -32,8 +26,7 @@ def ByteTable.completeness (x: F p) : x.val < 256 → ByteTable.contains (vec [x
   dsimp [Table.contains, ByteTable]
   use x.val
   simp [from_byte]
-  dsimp [vec]
-  rw [←Vector.vec_eq]
+  ext1
   have h' : (x.val) % 256 = x.val := by
     rw [Nat.mod_eq_iff_lt]; assumption; norm_num
   simp [h']
diff --git a/Clean/Types/Byte.lean b/Clean/Types/Byte.lean
index c532ce0..742a56d 100644
--- a/Clean/Types/Byte.lean
+++ b/Clean/Types/Byte.lean
@@ -1,14 +1,5 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Utils.Field
 import Clean.GadgetsNew.ByteLookup
 
-
 section
 variable {p : ℕ} [Fact (p ≠ 0)] [Fact p.Prime]
 variable [p_large_enough: Fact (p > 512)]
diff --git a/Clean/Types/U32.lean b/Clean/Types/U32.lean
index a7818b1..86e7c51 100644
--- a/Clean/Types/U32.lean
+++ b/Clean/Types/U32.lean
@@ -1,11 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Utils.Field
 import Clean.GadgetsNew.ByteLookup
 
 section
diff --git a/Clean/Utils/Vector.lean b/Clean/Utils/Vector.lean
index 9d2fda8..cc25d31 100644
--- a/Clean/Utils/Vector.lean
+++ b/Clean/Utils/Vector.lean
@@ -1,4 +1,6 @@
 import Mathlib.Data.Fintype.Basic
+import Mathlib.Tactic.Basic
+import Mathlib.Data.ZMod.Basic
 
 variable {α β : Type} {n : ℕ}
 
@@ -11,42 +13,36 @@ instance [Repr α] {n: ℕ} : Repr (Vector α n) where
 def vec (l: List α) : Vector α l.length := ⟨ l, rfl ⟩
 
 namespace Vector
-  theorem vec_eq (l : ℕ) (v w: Vector α l) : v.val = w.val ↔ v = w := by
-    constructor
-    · intro h
-      cases v
-      cases w
-      simp [Subtype.mk_eq_mk] at h
-      simp [h]
-    · aesop
-
-  theorem length_matches (v: Vector α n) : v.1.length = n := v.2
+  @[ext]
+  theorem ext (l : ℕ) (v w: Vector α l) : v.val = w.val → v = w := by
+    intro h
+    cases v
+    cases w
+    simp [Subtype.mk_eq_mk] at h
+    simp [h]
 
   @[simp]
   def map (f: α → β) : Vector α n → Vector β n
     | ⟨ l, h ⟩ => ⟨ l.map f, by rw [List.length_map, h] ⟩
 
-  @[simp]
-  def zip : Vector α n → Vector β n → Vector (α × β) n
+  def zip {n} : Vector α n → Vector β n → Vector (α × β) n
     | ⟨ [], ha ⟩, ⟨ [], _ ⟩  => ⟨ [], ha ⟩
-    | ⟨ a::as, ha ⟩, ⟨ b::bs, hb ⟩ => ⟨ (a, b) :: List.zip as bs, by sorry ⟩
+    | ⟨ a::as, (ha : as.length + 1 = n) ⟩,
+      ⟨ b::bs, (hb : bs.length + 1 = n) ⟩ =>
+      let ⟨ z, hz ⟩ := zip ⟨ as, rfl ⟩ ⟨ bs, by apply Nat.add_one_inj.mp; rw [ha, hb] ⟩
+      ⟨ (a, b) :: z, by show z.length + 1 = n; rw [hz, ha] ⟩
 
   @[simp]
   def get (v: Vector α n) (i: Fin n) : α :=
-    let i' : Fin v.1.length := Fin.cast (length_matches v).symm i
+    let i' : Fin v.1.length := Fin.cast v.prop.symm i
     v.val.get i'
 
   -- map over monad
-  @[simp]
-  def mapM { M : Type → Type } [Monad M] (v : Vector (M α) n) : M (Vector α n) :=
-    -- there `List.mapM` which we can use, but there doesn't seem to be an equivalent of `List.length_map` for monads
-    do
-      let l' ← List.mapM id v.val
-      return ⟨ l', by sorry ⟩
-
-  -- other direction
-  @[simp]
-  def unmapM { M : Type → Type } [Monad M] (v : M (Vector α n)) : Vector (M α) n :=
-    sorry
-
+  def mapM {M : Type → Type} {n} [Monad M] (v : Vector (M α) n) : M (Vector α n) :=
+    match (v : Vector (M α) n) with
+    | ⟨ [], h ⟩ => pure ⟨ [], h ⟩
+    | ⟨ a :: as, (h : as.length + 1 = n) ⟩ => do
+      let hd ← a
+      let tl ← mapM ⟨ as, rfl ⟩
+      pure ⟨ hd :: tl.val, by rwa [List.length_cons, tl.prop]⟩
 end Vector