have 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) ((xhi.toNat H + xlo.toNat H) * (yhi.toNat H + ylo.toNat H)) :=
  toNat_inj (H := (()::()::H))
    (((karatsubaHelper₃_toNat _ _ _  karatsuba_toNat).trans
      (congrArg₂ _
        (addWithCarry_eq_add₀ _ _)
        (addWithCarry_eq_add₀ _ _))).trans
      (toNat_ofNat_lt (mul_lt_bound_cons
        (add_lt_bound_cons (toNat_lt _) (toNat_lt _))
         (add_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
⊢ 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))
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))