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 const In_rec_ii : (set (set set set) set set) set set set axiom In_rec_G_ii_In_rec_ii: !P:set (set set set) set set.(!x:set.!g:set set set.!h:set set set.(!y:set.y iIn x -> g y = h y) -> P x g = P x h) -> !x:set.In_rec_G_ii P x (In_rec_ii P x) claim !P:set (set set set) set set.(!x:set.!g:set set set.!h:set set set.(!y:set.y iIn x -> g y = h y) -> P x g = P x h) -> !x: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 (P x (In_rec_ii P))