diff --git a/ArkLib.lean b/ArkLib.lean
index 8f5e8c4c9..45bb7e3c5 100644
--- a/ArkLib.lean
+++ b/ArkLib.lean
@@ -1,9 +1,11 @@
 import ArkLib.AGM.Basic
 import ArkLib.CommitmentScheme.Basic
 import ArkLib.CommitmentScheme.Fold
-import ArkLib.CommitmentScheme.InductiveMerkleTree
 import ArkLib.CommitmentScheme.KZG
 import ArkLib.CommitmentScheme.MerkleTree
+import ArkLib.CommitmentScheme.MerkleTree.Completeness
+import ArkLib.CommitmentScheme.MerkleTree.Defs
+import ArkLib.CommitmentScheme.MerkleTree.Extractability
 import ArkLib.CommitmentScheme.SimpleRO
 import ArkLib.CommitmentScheme.Tensor
 import ArkLib.CommitmentScheme.Trivial
diff --git a/ArkLib/CommitmentScheme/MerkleTree/Completeness.lean b/ArkLib/CommitmentScheme/MerkleTree/Completeness.lean
new file mode 100644
index 000000000..45e8ff032
--- /dev/null
+++ b/ArkLib/CommitmentScheme/MerkleTree/Completeness.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import ArkLib.CommitmentScheme.MerkleTree.Defs
+
+/-!
+# Inductive Merkle Tree Completeness
+
+-/
+
+
+namespace InductiveMerkleTree
+
+open List OracleSpec OracleComp BinaryTree
+
+variable {α : Type}
+
+/--
+A functional form of the completeness theorem for Merkle trees.
+This references the functional versions of `getPutativeRoot` and `buildMerkleTree_with_hash`
+-/
+theorem functional_completeness (α : Type) {s : Skeleton}
+  (idx : SkeletonLeafIndex s)
+  (leaf_data_tree : LeafData α s)
+  (hash : α → α → α) :
+  (getPutativeRoot_with_hash
+    idx
+    (leaf_data_tree.get idx)
+    (generateProof
+      (buildMerkleTree_with_hash leaf_data_tree hash) idx)
+    (hash)) =
+  (buildMerkleTree_with_hash leaf_data_tree hash).getRootValue := by
+  induction s with
+  | leaf =>
+    match leaf_data_tree with
+    | LeafData.leaf a =>
+      cases idx with
+      | ofLeaf =>
+        simp [buildMerkleTree_with_hash, getPutativeRoot_with_hash]
+  | internal s_left s_right left_ih right_ih =>
+    match leaf_data_tree with
+    | LeafData.internal left right =>
+      cases idx with
+      | ofLeft idxLeft =>
+        simp_rw [LeafData.get_ofLeft, LeafData.leftSubtree_internal, buildMerkleTree_with_hash,
+          generateProof_ofLeft, FullData.rightSubtree, FullData.leftSubtree,
+          getPutativeRoot_with_hash, left_ih, FullData.internal_getRootValue]
+      | ofRight idxRight =>
+        simp_rw [LeafData.get_ofRight, LeafData.rightSubtree_internal, buildMerkleTree_with_hash,
+          generateProof_ofRight, FullData.leftSubtree, FullData.rightSubtree,
+          getPutativeRoot_with_hash, right_ih, FullData.internal_getRootValue]
+
+
+/--
+Completeness theorem for Merkle trees.
+
+The proof proceeds by reducing to the functional completeness theorem by a theorem about
+the OracleComp monad,
+and then applying the functional version of the completeness theorem.
+-/
+theorem completeness [DecidableEq α] [SelectableType α] {s}
+    (leaf_data_tree : LeafData α s) (idx : BinaryTree.SkeletonLeafIndex s)
+    (preexisting_cache : (spec α).QueryCache) :
+    (((do
+      let cache ← buildMerkleTree leaf_data_tree
+      let proof := generateProof cache idx
+      let verified ← verifyProof idx (leaf_data_tree.get idx) (cache.getRootValue) proof
+      guard verified
+      ).simulateQ (randomOracle)).run preexisting_cache).neverFails := by
+  -- An OracleComp is never failing on any preexisting cache
+  -- if it never fails when run with any oracle function.
+  revert preexisting_cache
+  rw [randomOracle_neverFails_iff_runWithOracle_neverFails]
+  -- Call this hash function `f`
+  intro f
+  -- Simplify
+  simp only [verifyProof, bind_pure_comp, guard_eq, bind_map_left, beq_iff_eq, runWithOracle_bind,
+    runWithOracle_buildMerkleTree, runWithOracle_getPutativeRoot, apply_ite, runWithOracle_pure,
+    runWithOracle_failure, Option.bind_eq_bind, Option.bind_some, Option.isSome_some,
+    Option.isSome_none, Bool.if_false_right, Bool.and_true, decide_eq_true_eq]
+  exact functional_completeness α idx leaf_data_tree fun left right ↦ f () (left, right)
+
+end InductiveMerkleTree
diff --git a/ArkLib/CommitmentScheme/InductiveMerkleTree.lean b/ArkLib/CommitmentScheme/MerkleTree/Defs.lean
similarity index 75%
rename from ArkLib/CommitmentScheme/InductiveMerkleTree.lean
rename to ArkLib/CommitmentScheme/MerkleTree/Defs.lean
index d2b171930..7c334e851 100644
--- a/ArkLib/CommitmentScheme/InductiveMerkleTree.lean
+++ b/ArkLib/CommitmentScheme/MerkleTree/Defs.lean
@@ -6,8 +6,6 @@ Authors: Quang Dao
 
 import VCVio
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Basic
-import ArkLib.CommitmentScheme.Basic
-import Mathlib.Data.Vector.Snoc
 import ArkLib.ToVCVio.Oracle
 
 /-!
@@ -25,7 +23,7 @@ as defined in `ArkLib.Data.IndexedBinaryTree`.
 * We found that the inductive definition seems likely to be convenient for a few reasons:
   * It allows us to handle non-perfect trees.
   * It can allow us to use trees of arbitrary structure in the extractor.
-* I considered the indexed type useful because the completeness theorem and extractibility theorems
+* I considered the indexed type useful because the completeness theorem and Extractability theorems
   take indices or sets of indices as parameters,
   and because we are working with trees of arbitrary structure,
   this lets us avoid having to check that these indices are valid.
@@ -38,11 +36,15 @@ as defined in `ArkLib.Data.IndexedBinaryTree`.
   - [x] `getPutativeRoot`
   - [x] `verifyProof`
 - [x] Completeness theorem
+  - Note that we handle only single-branch proofs, without multi-leaf proofs.
+  - See SNARGs book 29.2 for the "path-pruning" optimization.
+  - See [here](https://eprint.iacr.org/2021/281.pdf#page=7.03) or [here](https://dev.risczero.com/proof-system-in-detail.pdf) for a slightly different approach ("Merkle caps"/"chopped Merkle trees") used in practice.
 - [ ] Collision Lemma (See SNARGs book 18.3)
   - (this is really not a lemma about oracles, so it could go with the binary tree API)
-- [ ] Extractibility (See SNARGs book 18.5)
+- [ ] Extractability (See SNARGs book 18.5)
+- [ ] Leaf type distinct from hash type
 - [ ] Multi-leaf proofs
-- [ ] Arbirary arity trees
+- [ ] Arbitrary arity trees
 - [ ] Multi-instance
 
 -/
@@ -248,77 +250,12 @@ lemma runWithOracle_getPutativeRoot {s} (idx : BinaryTree.SkeletonLeafIndex s)
 Verify a Merkle proof `proof` that a given `leaf` at index `i` is in the Merkle tree with given
 `root`.
 Works by computing the putative root based on the branch, and comparing that to the actual root.
-Outputs `failure` if the proof is invalid.
+Returns a boolean true/false depending on whether the proof is valid or not
 -/
 def verifyProof {α} [DecidableEq α] {s}
     (idx : BinaryTree.SkeletonLeafIndex s) (leafValue : α) (rootValue : α)
-    (proof : List α) : OracleComp (spec α) Unit := do
+    (proof : List α) : OracleComp (spec α) Bool := do
   let putative_root ← getPutativeRoot idx leafValue proof
-  guard (putative_root = rootValue)
-
-/--
-A functional form of the completeness theorem for Merkle trees.
-This references the functional versions of `getPutativeRoot` and `buildMerkleTree_with_hash`
--/
-theorem functional_completeness (α : Type) {s : Skeleton}
-  (idx : SkeletonLeafIndex s)
-  (leaf_data_tree : LeafData α s)
-  (hash : α → α → α) :
-  (getPutativeRoot_with_hash
-    idx
-    (leaf_data_tree.get idx)
-    (generateProof
-      (buildMerkleTree_with_hash leaf_data_tree hash) idx)
-    (hash)) =
-  (buildMerkleTree_with_hash leaf_data_tree hash).getRootValue := by
-  induction s with
-  | leaf =>
-    match leaf_data_tree with
-    | LeafData.leaf a =>
-      cases idx with
-      | ofLeaf =>
-        simp [buildMerkleTree_with_hash, getPutativeRoot_with_hash]
-  | internal s_left s_right left_ih right_ih =>
-    match leaf_data_tree with
-    | LeafData.internal left right =>
-      cases idx with
-      | ofLeft idxLeft =>
-        simp_rw [LeafData.get_ofLeft, LeafData.leftSubtree_internal, buildMerkleTree_with_hash,
-          generateProof_ofLeft, FullData.rightSubtree, FullData.leftSubtree,
-          getPutativeRoot_with_hash, left_ih, FullData.internal_getRootValue]
-      | ofRight idxRight =>
-        simp_rw [LeafData.get_ofRight, LeafData.rightSubtree_internal, buildMerkleTree_with_hash,
-          generateProof_ofRight, FullData.leftSubtree, FullData.rightSubtree,
-          getPutativeRoot_with_hash, right_ih, FullData.internal_getRootValue]
-
-
-/--
-Completeness theorem for Merkle trees.
-
-The proof proceeds by reducing to the functional completeness theorem by a theorem about
-the OracleComp monad,
-and then applying the functional version of the completeness theorem.
--/
-theorem completeness [DecidableEq α] [SelectableType α] {s}
-    (leaf_data_tree : LeafData α s) (idx : BinaryTree.SkeletonLeafIndex s)
-    (preexisting_cache : (spec α).QueryCache) :
-    (((do
-      let cache ← buildMerkleTree leaf_data_tree
-      let proof := generateProof cache idx
-      let _ ← verifyProof idx (leaf_data_tree.get idx) (cache.getRootValue) proof
-      ).simulateQ (randomOracle)).run preexisting_cache).neverFails := by
-  -- An OracleComp is never failing on any preexisting cache
-  -- if it never fails when run with any oracle function.
-  revert preexisting_cache
-  rw [randomOracle_neverFails_iff_runWithOracle_neverFails]
-  -- Call this hash function `f`
-  intro f
-  -- Simplify
-  simp_rw [verifyProof, guard_eq, bind_pure_comp, id_map', runWithOracle_bind,
-    runWithOracle_buildMerkleTree, runWithOracle_getPutativeRoot]
-  simp only [apply_ite, runWithOracle_pure, runWithOracle_failure, Option.bind_eq_bind,
-    Option.bind_some, Option.isSome_some, Option.isSome_none, Bool.if_false_right, Bool.and_true,
-    decide_eq_true_eq]
-  exact functional_completeness α idx leaf_data_tree fun left right ↦ f () (left, right)
+  return (putative_root == rootValue)
 
 end InductiveMerkleTree
diff --git a/ArkLib/CommitmentScheme/MerkleTree/Extractability.lean b/ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
new file mode 100644
index 000000000..90301a4b9
--- /dev/null
+++ b/ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
@@ -0,0 +1,343 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import ArkLib.CommitmentScheme.MerkleTree.Defs
+
+/-!
+# Inductive Merkle Tree Extractability
+
+-/
+
+open scoped NNReal
+
+/--
+Convert a computation to one that also returns its query log
+
+TODO
+- generalize Type universe?
+- generalize spec
+- move to vcv?
+- already in vcv?
+-/
+def OracleComp.withLogging {T : Type} (spec : OracleSpec Unit) (oa : OracleComp (spec) T) :
+    OracleComp (spec) (T × (spec).QueryLog) :=
+  (simulateQ loggingOracle oa).run
+
+/--
+prove that logging of a bind is bind of loggings.
+-/
+lemma OracleComp.pure_withLogging (A B) (spec : OracleSpec Unit)
+    (oa : OracleComp (spec) A) (ob : A → OracleComp (spec) B) :
+    (oa >>= ob).withLogging =
+    do
+      let (a, a_log) ← oa.withLogging
+      let (b, b_log) ← (ob a).withLogging
+      return (b, a_log ++ b_log) := by
+  sorry
+
+/--
+prove that logging of a bind is bind of loggings.
+-/
+lemma OracleComp.bind_withLogging (A B) (spec : OracleSpec Unit)
+    (oa : OracleComp (spec) A) (ob : A → OracleComp (spec) B) :
+    (oa >>= ob).withLogging =
+    do
+      let (a, a_log) ← oa.withLogging
+      let (b, b_log) ← (ob a).withLogging
+      return (b, a_log ++ b_log) := by
+  sorry
+
+namespace InductiveMerkleTree
+
+open List OracleSpec OracleComp BinaryTree
+
+variable {α : Type}
+
+def populate_down_tree {α : Type} (s : Skeleton)
+    (children : α → (α × α))
+    (root : α) :
+    FullData α s :=
+  match s with
+  | .leaf => FullData.leaf root
+  | .internal s_left s_right =>
+    let ⟨left_root, right_root⟩ := children root
+    FullData.internal
+      root
+      (populate_down_tree s_left children left_root)
+      (populate_down_tree s_right children right_root)
+
+/--
+The extraction algorithm for Merkle trees.
+
+This algorithm takes a merkle tree cache, a root, and a skeleton, and
+returns (optionally?) a FullData of Option α.
+
+* It starts with the root and constructs a tree down to the leaves.
+* If a node is not in the cache, its children are None
+* If a node is in the cache twice (a collision), its children are None
+* If a node is None, its children are None
+* Otherwise, a nodes children are the children in the cache.
+
+
+TODO, if there is a collision, but it isn't used or is only used in a subtree,
+should the rest of the tree work? Or should it all fail?
+-/
+def extractor {α : Type} [DecidableEq α] [SelectableType α] [Fintype α] [(spec α).FiniteRange]
+    (s : Skeleton)
+    (cache : (spec α).QueryLog)
+    (root : α) :
+    FullData (Option α) s :=
+  let queries := cache.getQ ();
+  let children (node : Option α) : (Option α × Option α) :=
+    match node with
+    | none => (none, none)
+    | some a =>
+      -- Find the first query resulting in this value
+    match queries.find? (fun ⟨_, r⟩ => r == a) with
+      | none => (none, none)
+      | some q =>
+        let child_hashes := q.1;
+        (some child_hashes.1, some child_hashes.2)
+  populate_down_tree s children (some root)
+
+/--
+The game for extractability.
+-/
+def extractability_game
+    [DecidableEq α] [SelectableType α] [Fintype α] [(spec α).FiniteRange]
+    {s : Skeleton}
+    {AuxState : Type}
+    (committingAdv : OracleComp (spec α)
+        (α × AuxState))
+    (openingAdv : AuxState →
+        OracleComp (spec α) (SkeletonLeafIndex s × α × List α)) :
+    OracleComp (spec α)
+      (α × AuxState × SkeletonLeafIndex s × α × List α ×
+       FullData (Option α) s × List (Option α) × Bool) :=
+  do
+    let ((root, aux), queryLog) ← committingAdv.withLogging
+    let extractedTree := extractor s queryLog root
+    let (idx, leaf, proof) ← openingAdv aux
+    let extractedProof := generateProof extractedTree idx
+    let verified ← verifyProof idx leaf root proof
+    return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified)
+
+
+
+/--
+The game for extractability, augmented to return the query logs
+of the committing adversary, opening adversary, and verification.
+-/
+def extractability_game_with_logging
+    [DecidableEq α] [SelectableType α] [Fintype α] [(spec α).FiniteRange]
+    {s : Skeleton}
+    {AuxState : Type}
+    (committingAdv : OracleComp (spec α)
+        (α × AuxState))
+    (openingAdv : AuxState →
+        OracleComp (spec α) (SkeletonLeafIndex s × α × List α)) :
+    OracleComp (spec α)
+      (α × AuxState × SkeletonLeafIndex s × α × List α ×
+       FullData (Option α) s × List (Option α) × Bool ×
+       (spec α).QueryLog × (spec α).QueryLog × (spec α).QueryLog)
+         :=
+  do
+    let ((root, aux), committingLog) ← (committingAdv).withLogging
+    let extractedTree := extractor s committingLog root
+    let ((idx, leaf, proof), openingLog) ← ((openingAdv aux)).withLogging
+    let extractedProof := generateProof extractedTree idx
+    let (verified, verificationLog) ←
+      ((verifyProof idx leaf root proof)).withLogging
+    return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+            committingLog, openingLog, verificationLog)
+
+
+
+
+-- Does this exists in vcvio somewhere?
+def collisionIn {α : Type} [DecidableEq α]
+    (log : (spec α).QueryLog) : Prop :=
+  ∃ q1 q2, (q1 ≠ q2) ∧
+    q1 ∈ log.getQ () ∧ q2 ∈ log.getQ () ∧
+    q1.2 == q2.2
+
+
+
+/--
+The extractability theorem for Merkle trees.
+
+Adapting from the SNARGs book Lemma 18.5.1:
+
+For any query bound `qb`,
+and for any adversary `committingAdv` that outputs a root and auxiliary data
+and any `openingAdv` that takes the auxiliary data and outputs a leaf index, leaf value, and proof,
+such that committingAdv and openingAdv together obey the query bound `qb`.
+
+If the `committingAdv` and `openingAdv` are executed, and the `extractor` algorithm is run on the
+resulting cache and root from `committingAdv`,
+then with probability at most κ
+does simultaneously
+
+* the merkle tree verification pass on the proof from `openingAdv`
+* with the extracted leaf value not matching the opened leaf value or the adversary producing a proof different from the extracted proof.
+
+Where κ is ≤ 1/2 * (qb - 1) * qb / (Fintype.card α)
+        + 2 * (s.depth + 1) * s.leafCount / (Fintype.card α)
+(For sufficiently large qb)
+
+Here, we loosen this a bit to attempt a proof by considering all collisions
+in the combined query logs of the committing and opening adversaries and the verification.
+-/
+theorem extractability [DecidableEq α] [SelectableType α] [Fintype α] [(spec α).FiniteRange]
+    {s : Skeleton}
+    {AuxState : Type}
+    (committingAdv : OracleComp (spec α)
+        (α × AuxState))
+    (openingAdv : AuxState →
+        OracleComp (spec α) (SkeletonLeafIndex s × α × List α))
+    (qb : ℕ)
+    (h_IsQueryBound_qb :
+      IsQueryBound
+        (do
+          let (root, aux) ← committingAdv
+          let (idx, leaf, proof) ← openingAdv aux
+          pure ()) qb)
+    (h_le_qb : 4 * s.leafCount + 1 ≤ qb)
+          :
+    [fun (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified) =>
+        verified ∧
+        (not (leaf == extractedTree.get idx.toNodeIndex)
+        ∨ not (proof.map (Option.some) == extractedProof)) |
+      do
+        let (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified) ←
+          extractability_game committingAdv openingAdv
+        return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified)
+      ] ≤
+        1/2 * ((qb + s.depth) - 1) * (qb + s.depth) / (Fintype.card α)
+        + 2 * (s.depth + 1) * s.leafCount / (Fintype.card α)
+    := by
+
+  calc
+    -- We first rewrite the game to include the query logs
+    _ = [fun (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+              committingLog, openingLog, verificationLog) =>
+            verified ∧
+            (not (leaf == extractedTree.get idx.toNodeIndex)
+            ∨ not (proof.map (Option.some) == extractedProof)) |
+          do
+            let (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                committingLog, openingLog, verificationLog) ←
+              extractability_game_with_logging committingAdv openingAdv
+            return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                    committingLog, openingLog, verificationLog)] := by
+      -- This follows from marginalization
+      sorry
+    -- The bad event happens only when there is a collision event
+    -- or the bad event happens with no collision
+    _ ≤ [fun (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+            committingLog, openingLog, verificationLog)
+            =>
+            (collisionIn (committingLog ++ openingLog ++ verificationLog)) ∨
+            (¬ (collisionIn (committingLog ++ openingLog ++ verificationLog)) ∧
+            (verified ∧
+            (not (leaf == extractedTree.get idx.toNodeIndex)
+            ∨ not (proof.map (Option.some) == extractedProof)))) |
+          do
+            let (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                committingLog, openingLog, verificationLog) ←
+              extractability_game_with_logging committingAdv openingAdv
+            return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                    committingLog, openingLog, verificationLog)] := by
+      apply probEvent_mono
+      tauto
+    -- We apply the union bound
+    _ ≤ [fun (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+            committingLog, openingLog, verificationLog)
+            =>
+            (collisionIn (committingLog ++ openingLog ++ verificationLog)) |
+          do
+            let (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                committingLog, openingLog, verificationLog) ←
+              extractability_game_with_logging committingAdv openingAdv
+            return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                    committingLog, openingLog, verificationLog)] +
+        [fun (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+            committingLog, openingLog, verificationLog)
+            =>
+            (¬ (collisionIn (committingLog ++ openingLog ++ verificationLog)) ∧
+            (verified ∧
+            (not (leaf == extractedTree.get idx.toNodeIndex)
+            ∨ not (proof.map (Option.some) == extractedProof)))) |
+          do
+            let (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                committingLog, openingLog, verificationLog) ←
+              extractability_game_with_logging committingAdv openingAdv
+            return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                    committingLog, openingLog, verificationLog)] := by
+        -- TODO is this in vcvio somewhere?
+        sorry
+    -- We bound the collision event probability with a collision bound
+    _ ≤ 1/2 * ((qb + s.depth) - 1) * (qb + s.depth) / (Fintype.card α) +
+        [fun (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+            committingLog, openingLog, verificationLog)
+            =>
+            (¬ (collisionIn (committingLog ++ openingLog ++ verificationLog)) ∧
+            (verified ∧
+            (not (leaf == extractedTree.get idx.toNodeIndex)
+            ∨ not (proof.map (Option.some) == extractedProof)))) |
+          do
+            let (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                committingLog, openingLog, verificationLog) ←
+              extractability_game_with_logging committingAdv openingAdv
+            return (root, aux, idx, leaf, proof, extractedTree, extractedProof, verified,
+                    committingLog, openingLog, verificationLog)] := by
+        gcongr
+        -- TODO: Prove a general collision bound lemma
+        sorry
+    -- We bound the no-collision bad event probability
+    _ ≤ 1/2 * ((qb + s.depth) - 1) * (qb + s.depth) / (Fintype.card α) +
+        2 * (s.depth + 1) * s.leafCount / (Fintype.card α):= by
+        sorry
+
+
+  /-
+  Now we can break down the bad event into smaller events
+  In the SNARGS book, they define
+  E_col = the event that there is a collision in committingLog
+  E_tree = the event that the tree extraction with committingLog
+           is different from the tree extraction
+           with the combined committingLog and openingLog
+  E_sub = the event that The verificationLog contains a query to a node not in the committingLog
+          and verification succeeds
+
+  The SNARGs book makes the observation that
+
+  Pr[Adversary wins] ≤ Pr[E_col]
+                       + Pr[E_tree | not E_col]
+                       + Pr[E_sub | not E_col and not E_tree]
+                       + Pr[Adversary wins | not E_col and not E_tree and not E_sub]
+
+  But I think this really stands in for the tighter version, which might be easier to reason about.
+
+  Pr[Adversary wins] ≤ Pr[E_col]
+                       + Pr[E_tree and not E_col]
+                       + Pr[E_sub and not E_col and not E_tree]
+                       + Pr[Adversary wins and not E_col and not E_tree and not E_sub]
+
+  TODO: does the proof really have to be this complicated?
+  Can't we simply look at the event of any collision at all happening?
+
+  * Does a collision happen in the adversary's queries and verification combined?
+    * Probability of YES is small by query bound
+    * If not, then consider whether the index opened exists in the extracted tree.
+      * If yes, then if the proof differs at all, we must leave the extracted tree
+        * After which, we can't return without a collision, so we don't verify.
+      * If no, then the only way to verify is to have a collision.
+
+  -/
+
+
+end InductiveMerkleTree
diff --git a/ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean b/ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean
index 4a43258f5..715c7e0cd 100644
--- a/ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean
+++ b/ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean
@@ -100,6 +100,24 @@ def SkeletonInternalIndex.toNodeIndex {s : Skeleton} (idx : SkeletonInternalInde
 
 end Skeleton
 
+section Count
+
+def Skeleton.leafCount : Skeleton → Nat
+  | Skeleton.leaf => 1
+  | Skeleton.internal left right =>
+    left.leafCount + right.leafCount
+
+end Count
+
+section Depth
+
+def Skeleton.depth : Skeleton → Nat
+  | Skeleton.leaf => 0
+  | Skeleton.internal left right =>
+    Nat.max left.depth right.depth + 1
+
+end Depth
+
 /-!
 This section contains predicates about indices determined by their neighborhood in the tree.
 -/