const In : set set prop term iIn = In infix iIn 2000 2000 const Sigma : set (set set) set const proj0 : set set axiom proj0_Sigma: !x:set.!f:set set.!y:set.y iIn Sigma x f -> proj0 y iIn x const ap : set set set const Empty : set axiom proj0_ap_0: !x:set.proj0 x = ap x Empty claim !x:set.!f:set set.!y:set.y iIn Sigma x f -> ap y Empty iIn x