The set closure pair(s, f) is closed under f.

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

Proof that closure pair(s, f) is closed under f | OTTER output file

up show outline