have h: ∀ {H: List Unit} {x y: BitTree} [Perfect H x] [Perfect H y], x.toNat H * y.toNat H % (bound (()::H)) = x.toNat H * y.toNat H :=
  Nat.mod_eq_of_lt (lt_of_lt_of_eq (Nat.mul_lt_mul_for_real (toNat_lt _) (toNat_lt _)) (bound_cons _).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
⊢ 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 (() :: H) (node xhi xlo) (node yhi ylo) =
    ofNat (() :: () :: H) (toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo))