You could use set and unset, which have been used in Mathematica for the past 25 years.
In a programming language, a statement that changes the value of a variable is only meaningful if the variable is referenced at a later point in the program. In some languages, though, a symbolic expression in the language itself can be manipulated, e.g. differentiated with respect to its unbound variables. In such cases, the “setting” or “unsetting” of a variable alters the type of action that can be performed on the expression at a later stage.
Please think twice before you introduce a new word for an already familiar operation. I realize that existing languages are protected by patents and copyrights, and that some words may be legally unusable, but binding and unbinding are very basic concepts.
Edited to add:
@dalum Look at it this way: in a symbolic reasoning system, you can have an assertion that limits the range of values that can be assigned to a free variable. This corresponds only in part to the human action of assuming, but in the execution of the program there is no assumption, simply recording and calculation. One set of symbolic statements can be transformed into a different set, from which a different form of information can be obtained.
In the case you describe, you are removing an assertion about the free variable from your set of statements. However, there may be many assertions in the set, so it may not be possible to say anything at the higher semantic level about “disassuming”. There may be other assertions that implicity restrict the range of the free variable.
Also, don’t go by what you read in the literature in the words surrounding equations. Natural language and symbolic reasoning are different, and a lot of mathematics is closer to natural language than you might think. Otherwise, the Principia Mathematica would not have taken as long to write, or be as difficult to read.