diff --git a/ProvenZk/Merkle.lean b/ProvenZk/Merkle.lean
index 593c606..bfc7566 100644
--- a/ProvenZk/Merkle.lean
+++ b/ProvenZk/Merkle.lean
@@ -528,4 +528,23 @@ theorem recover_equivalence
     . apply recover_proof_reversible (Item := Item)
       assumption
 
+theorem eq_root_eq_tree {H} [ph: Fact (perfect_hash H)] {t₁ t₂ : MerkleTree α H d}:
+  t₁.root = t₂.root ↔ t₁ = t₂ := by
+  induction d with
+  | zero => cases t₁; cases t₂; tauto
+  | succ _ ih =>
+    cases t₁
+    cases t₂
+    apply Iff.intro
+    . intro h
+      have h := Fact.elim ph h
+      injection h with h
+      injection h with _ h
+      injection h
+      congr <;> {rw [←ih]; assumption}
+    . intro h
+      injection h
+      subst_vars
+      rfl
+
 end MerkleTree
diff --git a/ProvenZk/Misc.lean b/ProvenZk/Misc.lean
index 870ec71..e206567 100644
--- a/ProvenZk/Misc.lean
+++ b/ProvenZk/Misc.lean
@@ -44,4 +44,4 @@ lemma select_rw [Fact (Nat.Prime N)] {b i1 i2 out : (ZMod N)} : (Gates.select b
 
 lemma double_prop {a b c d : Prop} : (b ∧ a ∧ c ∧ a ∧ d) ↔ (b ∧ a ∧ c ∧ d) := by
   simp
-  tauto
\ No newline at end of file
+  tauto