const In : set set prop term iIn = In infix iIn 2000 2000 const Sigma : set (set set) set const setsum : set set set const proj0 : set set const proj1 : set set axiom Sigma_eta_proj0_proj1: !x:set.!f:set set.!y:set.y iIn Sigma x f -> setsum (proj0 y) (proj1 y) = y & proj0 y iIn x & proj1 y iIn f (proj0 y) claim !x:set.!f:set set.!y:set.y iIn Sigma x f -> ?z:set.z iIn x & ?w:set.w iIn f z & y = setsum z w