The closure contains the set.

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