Substitution

Nuprl's logic has a couple of rules for carrying out simple kinds of substitutions. These rules are accessible through the tactics described here. Occasionally these rules are useful; they can generate fewer and easier-to-solve well-formedness goals than the rewrite package.

Subst (eq:term) c

eq  should be a proposition of form . The effect of Subst is to replace all occurrences of t1 in clause c by t2. Three subgoals are generated; a main subgoal with the substitution carried out, a wf subgoal to prove functionality of the clause, and an equality subgoal to prove that .For example:



where is the inferred universe for clause c. Universe inference can be overridden by supplying an optional universe argument with the Using tactical.

HypSubst i c

Runs the Subst   tactic using the equality proposition in hypothesis i. Generates a wf subgoal and a main subgoal.

RevHypSubst i c

As HypSubst,  i c except that equality hypothesis is used right-to-left rather than left-to-right.

SubstClause t c

Replace clause c  with term t. Generates a main subgoal and an equality subgoal.