In language equivalence development we need to be able to calculate how many fresh worlds are there in Omega. With currently used implementation of FSets (from Metatheory) this cannot be done. Possible fixes: add length as a method for FSet object or change the representation into lists+uniqueness+permutation. The latter has the advantage of worlds names consistency while changing between labeled and label-free version (with just length we need to generate fresh names)
In language equivalence development we need to be able to calculate how many fresh worlds are there in Omega. With currently used implementation of FSets (from Metatheory) this cannot be done. Possible fixes: add length as a method for FSet object or change the representation into lists+uniqueness+permutation. The latter has the advantage of worlds names consistency while changing between labeled and label-free version (with just length we need to generate fresh names)