simp [toNat_node, rearrange, negate, add_toNat_negate _, ← Nat.mul_succ, Nat.succ_eq_add_one, bound_cons]
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
rearrange : ∀ {m a b c d e : ℕ}, m * a + b + (m * c + d) + e = m * (a + c) + (b + d + e)
⊢ toNat (() :: H✝) (node l✝ r✝) + toNat (() :: H✝) (negate (node l✝ r✝)) + 1 = bound (() :: H✝)
no goals