const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const ap : set set set const setsum : set set set axiom apE: !x:set.!y:set.!z:set.z iIn ap x y -> setsum y z iIn x const Sigma : set (set set) set axiom lamI: !x:set.!f:set set.!y:set.y iIn x -> !z:set.z iIn f y -> setsum y z iIn Sigma x f axiom apI: !x:set.!y:set.!z:set.setsum y z iIn x -> z iIn ap x y axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y lemma !x:set.!f:set set.!y:set.!z:set.z iIn ap (Sigma x f) y -> setsum y z iIn Sigma x f -> z iIn f y claim !x:set.!f:set set.!y:set.y iIn x -> ap (Sigma x f) y = f y