intro _ _ _ _ _ _
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
⊢ ∀ {m xh xl yh yl c : ℕ}, m * xh + xl + (m * yh + yl) + c = m * (xh + yh) + (xl + yl + c)
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
m✝ xh✝ xl✝ yh✝ yl✝ c✝ : ℕ
⊢ m✝ * xh✝ + xl✝ + (m✝ * yh✝ + yl✝) + c✝ = m✝ * (xh✝ + yh✝) + (xl✝ + yl✝ + c✝)