public static void constrainAsSubset(Proposition prop, Collection set1, Collection set2) {
    if (set1.length() > set2.length()) {
      Proposition.signalUnificationClash(prop, set1, set2);
    }
    { Cons copy1 = Stella.NIL;
      Cons copy2 = Stella.NIL;

      { Stella_Object i2 = null;
        Iterator iter000 = ((Iterator)(set2.allocateIterator()));

        while (iter000.nextP()) {
          i2 = iter000.value;
          copy2 = Cons.cons(i2, copy2);
        }
      }
      { Stella_Object i1 = null;
        Iterator iter001 = ((Iterator)(set1.allocateIterator()));

        while (iter001.nextP()) {
          i1 = iter001.value;
          if (copy2.memberP(i1)) {
            copy2 = copy2.remove(i1);
          }
          else {
            copy1 = Cons.cons(i1, copy1);
          }
        }
      }
      if (copy1 == Stella.NIL) {
        return;
      }
      if (copy2.length() == 1) {
        { Stella_Object item1 = copy1.value;
          Stella_Object item2 = copy2.value;

          Proposition.equateValues(prop, item1, item2);
          return;
        }
      }
      { int skolemcount1 = 0;
        int skolemcount2 = 0;

        { Stella_Object i1 = null;
          Cons iter002 = copy1;

          for (;!(iter002 == Stella.NIL); iter002 = iter002.rest) {
            i1 = iter002.value;
            if (Logic.skolemP(i1)) {
              skolemcount1 = skolemcount1 + 1;
            }
          }
        }
        { Stella_Object i2 = null;
          Cons iter003 = copy2;

          for (;!(iter003 == Stella.NIL); iter003 = iter003.rest) {
            i2 = iter003.value;
            if (Logic.skolemP(i2)) {
              skolemcount2 = skolemcount2 + 1;
            }
          }
        }
        if ((skolemcount1 + skolemcount2) == 0) {
          Proposition.signalUnificationClash(prop, set1, set2);
        }
      }
    }
  }