[PVS-Help] problem in induction scheme for lemmas involving 'choose'

```Hi,

I am trying to prove lemma pred_edge in following theory:

%%%%%%%%%%%%%%%%%%
grf  [node:TYPE+ ]: THEORY

BEGIN

mygraph: VAR non_empty_finite_set[[node, node]]
p, q: VAR node

%% recursive definition to find predecessors of node p in mygraph

predecessors(mygraph, p): RECURSIVE set[node] =
IF mygraph=emptyset  THEN emptyset
ELSE LET edge = choose(mygraph) IN
IF edge`2 = p THEN
ELSE
predecessors(remove(edge,mygraph), p)
ENDIF
ENDIF
MEASURE card(mygraph)

%%
% induction scheme :
% base case :emptyset
% induction step : assume for g_var and prove for (g_var + 1 edge)
%%

graph_induction: LEMMA
FORALL (p: [non_empty_finite_set[[node,node]] -> boolean]):
( p(emptyset) AND
(FORALL (g_var:non_empty_finite_set[[node,node]],a,b:node):
)
IMPLIES (FORALL (g_var: non_empty_finite_set[[node,node]]): p(g_var)))

pred_edge : LEMMA
predecessors(mygraph,p)(q) IFF member((q,p),mygraph)

END grf
%%%%%%%%%%%%%%%%%%

while proving this i reached a step which i think can not be proved due
to randomness of choose.

[-1]  choose(add((a!1, b!1), g_var!1))`2 = p!1
[-2]  member((q!1, p!1), add((a!1, b!1), g_var!1))
[-3]  predecessors(g_var!1, p!1)(q!1)
[-4]  member((q!1, p!1), g_var!1)
|-------
{1}   choose(add((a!1, b!1), g_var!1))`1 = q!1
{2}   member(q!1,