Get Putative Root With Hash binding

theorem getPutativeRootWithHash_binding    (h : α → α → α) {s : Skeleton} (idx : SkeletonLeafIndex s)    (proof₁ proof₂ : List.Vector α idx.depth) (x y : α)    (hne : x ≠ y)    (heq : getPutativeRootWithHash idx x proof₁ h         = getPutativeRootWithHash idx y proof₂ h) :    ∃ l₁ r₁ l₂ r₂, findCollision h idx proof₁ proof₂ x y = some (l₁, r₁, l₂, r₂) := by  induction idx generalizing x y with  | ofLeaf =>      simp only [getPutativeRootWithHash] at heq      exact absurd heq hne  | ofLeft idxLeft ih =>      simp only [getPutativeRootWithHash] at heq      by_cases hpair : (getPutativeRootWithHash idxLeft x proof₁.tail h, proof₁.head) =                       (getPutativeRootWithHash idxLeft y proof₂.tail h, proof₂.head)      · -- Pairs agree: recurse on the smaller index.        obtain ⟨hsub, _⟩ := Prod.mk.inj hpair        obtain ⟨l₁, r₁, l₂, r₂, hfind⟩ := ih proof₁.tail proof₂.tail x y hne hsub        exact ⟨l₁, r₁, l₂, r₂, by simp [findCollision, hpair, hfind]⟩      · -- Pairs differ but hash to the same value: top-level collision.        exact ⟨getPutativeRootWithHash idxLeft x proof₁.tail h, proof₁.head,               getPutativeRootWithHash idxLeft y proof₂.tail h, proof₂.head,               by simp [findCollision, hpair, heq]⟩  | ofRight idxRight ih =>      simp only [getPutativeRootWithHash] at heq      by_cases hpair : (proof₁.head, getPutativeRootWithHash idxRight x proof₁.tail h) =                       (proof₂.head, getPutativeRootWithHash idxRight y proof₂.tail h)      · -- Pairs agree: recurse on the smaller index.        obtain ⟨_, hsub⟩ := Prod.mk.inj hpair        obtain ⟨l₁, r₁, l₂, r₂, hfind⟩ := ih proof₁.tail proof₂.tail x y hne hsub        exact ⟨l₁, r₁, l₂, r₂, by simp [findCollision, hpair, hfind]⟩      · -- Pairs differ but hash to the same value: top-level collision.        exact ⟨proof₁.head, getPutativeRootWithHash idxRight x proof₁.tail h,               proof₂.head, getPutativeRootWithHash idxRight y proof₂.tail h,               by simp [findCollision, hpair, heq]⟩