const In : set set prop term iIn = In infix iIn 2000 2000 term In_rec_G_ii = \P:set (set set set) set set.\x:set.\f:set set.!Q:set (set set) prop.(!y:set.!g:set set set.(!z:set.z iIn y -> Q z (g z)) -> Q y (P y g)) -> Q x f claim !P:set (set set set) set set.!x:set.!g:set set set.(!y:set.y iIn x -> In_rec_G_ii P y (g y)) -> !Q:set (set set) prop.(!y:set.!h:set set set.(!z:set.z iIn y -> Q z (h z)) -> Q y (P y h)) -> Q x (P x g)