;; IVY operation: PROVE
;;
;; From basis S and K, show that a combinator Wxy=xyy exists.

(imp (and (all x (= x x))
	  (all x (all y (all z (= (a (a (a (S) x) y) z)
				  (a (a x z) (a y z))))))
	  (all x (all y (= (a (a (K) x) y) x))))

     (exists W (all x (all y (= (a (a W x) y) (a (a x y) y))))))