const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set const Empty : set axiom In_1_2: ordsucc Empty iIn ordsucc (ordsucc Empty) axiom neq_1_0: ordsucc Empty != Empty const If_i : prop set set set axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y const ap : set set set const Sigma : set (set set) set axiom beta: !x:set.!f:set set.!y:set.y iIn x -> ap (Sigma x f) y = f y claim !x:set.!y:set.ap (Sigma (ordsucc (ordsucc Empty)) \z:set.If_i (z = Empty) x y) (ordsucc Empty) = y