theorem grecaux20 (F K: set) (k x z: nat): $ grecaux2 z K F x 0 k = z $;
recn z (\\ a1, \ a2, F @ (a1, grecaux1 K x k (x - suc a1), a2)) 0 = z
grecaux2 z K F x 0 k = z