During our work on verification of Tezos source code,
we faced a problem: some proofs were taking too long time to execute.
For example, function which proves equality of `parse_ty_aux`

and
`dep_parse_ty_aux`

was executing about 5 minutes, according to CI
(Not acceptable! We couldn't even merge this proof!).

For the information why we actually needed to prove the equality of `parse_ty_aux`

and `dep_parse_ty_aux`

, and why we had to create a function-simulation
`dep_parse_ty_aux`

, please check this article:
Simulations - dependently-typed version

What is the reason of such a long execution period? First of all the length of
original `parse_ty_aux`

is about 500 lines of code. So the term itself is rather
big, and each step of its reduction is a time-taking procedure.

Many other functions that also need to be verified are even longer, for example
the Fixpoint `parse_data_aux`

is having 4932 lines of code. Therefore, it is
very important that the proofs for such a long functions are optimized.