Blum's speedup theorem is a statement about a certain class of computable functions for which it is always possible to find a program of lower complexity. Gödel's speed-up theorem is a statement about the possibility of drastically reducing the size of a theorem proof, by going to a more powerful axiomatic system.
Is Gödel's speed-up theorem an instance of Blum's speedup theorem, in which the computable function takes as input the axioms and outputs the theorem? Such a function could concretely be built in theorem proving programming languages, say for instance with Coq.
Additional info: I found this that looks related, but it doesn't clearly answer my question.