have h₁:
      (karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
          (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)))) =
      ofNat (()::()::H) (xlo.toNat H * yhi.toNat H + xhi.toNat H * ylo.toNat H) :=
    toNat_inj (H := (()::()::H))
      (((karatsubaHelper₁_toNat xhi xlo yhi ylo _ _ _ karatsuba_toNat karatsuba_toNat
        (toNat_ofNat_lt (mul_lt_bound_cons
          (add_lt_bound_cons (toNat_lt _) (toNat_lt _))
          (add_lt_bound_cons (toNat_lt _) (toNat_lt _))))).trans
        (add_comm _ _)).trans
        (toNat_ofNat_lt (add_lt_bound_cons
          (mul_lt_bound_cons (toNat_lt _) (toNat_lt _))
          (mul_lt_bound_cons (toNat_lt _) (toNat_lt _)))).symm)
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))