list(usable). a(subset,pair(a(p1,x),a(closure,x))) = p1. % (not used in later proofs) end_of_list.
Proof that the closure contains the set | OTTER output file
up | previous | next | detailed contents | brief contents