$$$A4.pvs
equality  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  x,y:VAR real
  a:real=1
  f(x,y):real = x+y
  g(x,y):real = x+y

  IbEx: THEOREM f(y,a)=g(y,1)
END equality

ch11E11  % [ parameters ]
		: THEORY
% Theory for Rubin Chapter 11 Question E11 on p. 244
  BEGIN

  U:TYPE+

  P:PRED[U]
  A,B,C,D:PRED[U]

  x,y : VAR U

  E11: THEOREM (FORALL x,y:A(x)&B(y)=> x=y)&(EXISTS x:A(x)&C(x))&
	(EXISTS x:B(x)&D(x))
	=>(EXISTS x:C(x)&D(x))

  END ch11E11



$$$A4.prf
(|equality| (|IbEx| "" (EXPAND* "f" "g") (("" (EXPAND* "a") NIL NIL)) NIL))
(|ch11E11|
 (E11 "" (FLATTEN)
  (("" (SKOLEM!)
    (("" (SKOLEM!)
      (("" (INST -1 "x!1" "x!2")
        (("" (FLATTEN)
          (("" (SPLIT)
            (("1" (INST 1 "x!1")
              (("1" (SPLIT)
                (("1" (PROPAX) NIL NIL)
                 ("2" (REPLACE -1 *) (("2" (PROPAX) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (PROPAX) NIL NIL) ("3" (PROPAX) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))