simp only [
toNat_node, lo, hi, lshift2, bound_cons,
left_distrib, right_distrib, ← mul_assoc,
mul_right_comm _ _ (bound H), mul_comm (toNat _ _) (bound H),
Nat.add_assoc, Nat.mul_add_mod,
toNat_zero, add_zero]
H : List Unit
left✝¹ right✝¹ left✝ right✝ : BitTree
lhs✝¹ : Perfect H left✝¹
rhs✝¹ : Perfect H right✝¹
lhs✝ : Perfect H left✝
rhs✝ : Perfect H right✝
⊢ toNat (() :: () :: H) (lshift2 H (node (node left✝¹ right✝¹) (node left✝ right✝))) % bound (() :: () :: H) =
    toNat (() :: () :: H) (node (node left✝¹ right✝¹) (node left✝ right✝)) * bound H % bound (() :: () :: H)
no goals