const ReplSep : set (set prop) (set set) set const setsum : set set set const proj1 : set set term ap = \x:set.\y:set.ReplSep x (\z:set.?w:set.z = setsum y w) proj1 const In : set set prop term iIn = In infix iIn 2000 2000 lemma !x:set.!y:set.!z:set.!w:set.!u:set.w iIn x -> w = setsum y u -> z = u -> w = setsum y z -> setsum y z iIn x var x:set var y:set var z:set var w:set var u:set hyp w iIn x hyp z = proj1 w hyp w = setsum y u claim z = u -> setsum y z iIn x