```Hello,

I got a big problem when I proved the following lemma. Because I don't
know too much prover commands, who could give me any suggestions.
That's so appreciated!

hide_para.1.2 :

[-1]  P2!1(t1!3)
[-2]  P1!1(t1!2)
[-3]  t1!1 = leak(t1!2, X!1)
[-4]  t2!1 = leak(t1!3, X!1)
{-5}  prod(A!1)(leak(t1!2, X!1), leak(t1!3, X!1), x!1)
[-6]  disjoint?(A!1, X!1)
|-------
[1]   EXISTS (t1_1:
({t: trace[E] |
EXISTS (t1: (P1!1), t2: (P2!1)):
prod(A!1)(t1, t2, t)})):
x!1 = leak(t1_1, X!1)

====================================================
ps: Here prod is a function in which t is observed as a result if t1
and t2 can be executed concurrently by two processes which synchronise
on A. Indeed, t,t1 and t2 are traces denoted as lists.

prod(A)(t1, t2, t) : RECURSIVE bool =
CASES t OF
null : null?(t1) AND null?(t2),
cons(x, y) :
IF A(x)
THEN
cons?(t1) AND cons?(t2) AND
car(t1) = x AND car(t2) = x
AND prod(A)(cdr(t1), cdr(t2), y)
ELSE
(cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y))
OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y))
ENDIF
ENDCASES
MEASURE length(t)

leak(t,A) is a function that gets rid of t's events included in set A
for example:

t: a->b->c-> Stop
A:{a,b}
leak(t,A)= c->Stop

ok, let's go back the above question. In 1.2, I can't use inst?
because I can't find a instance.  Please suggest me some commands to
make the prove carry on.

Many thanks!

Kun Wei

```