skeep

PVSのskeepコマンドは，本来は x!1 などのように新規に導入すべきスコーレム定数を，衝突がない限り束縛されていた変数と同じ名前で導入してくれます．

f1 :  

  |-------
{1}   (EXISTS (x: A): (p(x))) AND (EXISTS (x: A): (q(x))) =>
       (EXISTS (x: A): (p(x) AND (EXISTS (x: A): (q(x)))))

Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
f1 :  

{-1}  (EXISTS (x: A): (p(x)))
{-2}  (EXISTS (x: A): (q(x)))
  |-------
{1}   (EXISTS (x: A): (p(x) AND (EXISTS (x: A): (q(x)))))

Rule? (skeep*)
Iterating skeep in '*,
this simplifies to: 
f1 :  

{-1}  (p(x))
{-2}  (q(x!1))
  |-------
{1}   (EXISTS (x: A): (p(x) AND (EXISTS (x: A): (q(x)))))

Rule? (inst + "x")
Instantiating the top quantifier in + with the terms: 
 x,
this simplifies to: 
f1 :  

[-1]  (p(x))
[-2]  (q(x!1))
  |-------
{1}   (p(x) AND (EXISTS (x: A): (q(x))))

Rule? (split)
Splitting conjunctions,
this yields  2 subgoals: 
f1.1 :  

[-1]  (p(x))
[-2]  (q(x!1))
  |-------
{1}   p(x)

which is trivially true.

This completes the proof of f1.1.

f1.2 :  

[-1]  (p(x))
[-2]  (q(x!1))
  |-------
{1}   (EXISTS (x: A): (q(x)))

Rule? (inst + "x!1")
Instantiating the top quantifier in + with the terms: 
 x!1,

This completes the proof of f1.2.

Q.E.D.