for A being finite Subset of Vars
for i being Nat holds [(varcl A),i] in Vars