use(lists).

~ all(A,all(B,(

     car(g(A))=cdr(g(B))and A=B and f(A)=g(B)=>cons(car(g(B)),car(f(A)))=g(B)


     ))).