intro h₀ h₂ h₃
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
⊢ toNat (() :: H) z₀ = toNat H xlo * toNat H ylo →
    toNat (() :: H) z₂ = toNat H xhi * toNat H yhi →
      toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo) →
        toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) =
          toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi