(b) Removing an unproven axiom on conqueue
(c) Adding a free variable factory. Need to incorporate it so as to assert
freshness of newly created closures