[PVS-Help] partly replace

["=?gb2312?b?0O3H7Ln6?=" <qgxu@xxxxxxxxxxxxxxx>]

Hi everyone here:
   Can the prover command (repalce) complete replace some (not all) terms in a certain formula? 
For example, in the following pending sequent

[-1] a = b
[-2] c * a = c * a
|----
 {1} ....

How to convert fnum -2 into c * a = c* b using (replace) command or other command with the help of fnum -1? 

I have read the help message about (repalce) command, and haven't find the useful information.

thanks in advance.


Qingguo XU


                       qgxu@xxxxxxxxxxxxxxx
                       2008-05-22