Removal refers to the process of solving a problem or subproblem via a removal module. Removal always strictly simplifies the problem, by providing bindings for an open problem or by proving or failing to prove a closed problem.
Contrast this with transformation, which transforms a problem into one or more problems that may be more complex than the original.
See also removal link, removal modules, HL modules.