[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

CSP Libraries



Hello,
 
In CSP Libraries, I could prove
 
prod(A)(t1,t2,t)  AND A(a) AND t1=cons(a,u1) AND t2=cons(a,u2)   IMPLIES
                    EXISTS u: prod(A)(u1,u2,u) AND t=cons(a,u)
 
 
But When I was proving another LEMMA, I got problems.
 
prod(A)(t1,t2,t) AND A(a) AND t=cons(a,u) IMPLIES
            EXISTS u1,u2: prod(A)(u1,u2,u) AND t1= cons(a,u1) AND t2=cons(a,u2)
 
Anyboday could give me advises?
 
 
Kun