The set s is a subset of closure pair(s, f).

list(usable).
a(subset,pair(xs,a(closure,pair(xs,xf)))) = p1.
end_of_list.

Proof that s is a subset of closure pair(s, f) | OTTER output file

up show outline