The closure is closed under the function.

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 show outline