simp [bound_cons, toNatHelper, toNatHelper_acc H _ x, toNatHelper_acc H _ (_ + _),
  toNatHelper_acc H _ (toNatHelper _ _ _),
  left_distrib, right_distrib, ← mul_assoc, ← add_assoc]
H : List Unit
left✝ right✝ : BitTree
lhs✝ : Perfect H left✝
rhs✝ : Perfect H right✝
x : ℕ
⊢ toNatHelper (() :: H) (node left✝ right✝) x = bound (() :: H) * x + toNatHelper (() :: H) (node left✝ right✝) 0
no goals