Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }