You can reduce a proof by finding the term that corresponds to it, finding a term \alpha equivalent to that term, and then reconstructing a proof from the equivalent term.

A proof is a candidate for reduction whenever an implication is introduced and then immediately used as either premise of a use of \rightarrowE

Reducing a proof will never change its conclusion.

You can reduce a proof by finding the term that corresponds to it, \beta reducing the term, and then reconstructing a proof from the reduced term.

Reducing a proof will never change its open assumptions.