proveit.
traverse_inner_expressions
A simple algorithm to yield all inner expressions of an expression, including the expression itself. These will be reported in a depth- first order.