pairs[T: TYPE]: THEORY BEGIN x,y,v,z: VAR T pair: TYPE = [T,T] mk_pair(x,y): pair = (x,y) mk_pair_eq: LEMMA mk_pair(x,y) = mk_pair(v,z) IMPLIES (x = v AND y = z) in?(z:T, p: pair): bool = LET (x,y) = p IN z = x OR z = y apair?(x,y): bool = (x /= y) apair: TYPE = {p: pair | LET (x,y) = p IN x /= y} ap: VAR apair apair_irreflexive : LEMMA LET (x,y) = ap IN x /= y END pairs