const SetAdjoin : set set set const Sing : set set const ordsucc : set set const Empty : set const In : set set prop term iIn = In infix iIn 2000 2000 const ordinal : set prop var x:set var y:set var z:set hyp ordinal x hyp ordinal y hyp z iIn x hyp SetAdjoin y (Sing (ordsucc Empty)) = SetAdjoin z (Sing (ordsucc Empty)) claim y = z -> y iIn x