const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const nat_p : set prop var p:set prop hyp !x:set.nat_p x -> (!y:set.y iIn x -> p y) -> p x claim (!x:set.nat_p x -> !y:set.y iIn x -> p y) -> !x:set.nat_p x -> p x