have karatsuba_toNat: ∀ {x y} [Perfect H x] [Perfect H y], toNat (()::H) (karatsuba H x y) = x.toNat H * y.toNat H :=
  (congrArg _ (karatsuba_eq_mul _ _ _)).trans ((toNat_ofNat _ _).trans h)
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 (() :: 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
⊢ karatsuba (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))