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