∀ (env : Lean.Kernel.Environment) (decl : Lean.Declaration) (givenType : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.declTypeMismatch env decl givenType) = 1 + sizeOf env + sizeOf decl + sizeOf givenType