const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const Empty : set lemma !P:prop.Empty = Empty | P -> P | ~ P claim !P:prop.P | ~ P