(a) Improving the model so that acyclicity properties of ADTs are provable

(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