const Empty : set const nat_p : set prop const ordsucc : set set axiom nat_ind: !p:set prop.p Empty -> (!x:set.nat_p x -> p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x claim !p:set prop.p Empty -> (!x:set.nat_p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x