public static Cons propositionToCons(Proposition prop) {
    { Cons result = Stella.NIL;

      { Stella_Object arg = null;
        Vector vector000 = prop.arguments;
        int index000 = 0;
        int length000 = vector000.length();

        for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          result = Cons.cons(Logic.consifyArgument(arg), result);
        }
      }
      { Keyword testValue000 = prop.kind;

        if (testValue000 == Logic.KWD_IN) {
          return (result);
        }
        else if ((testValue000 == Logic.KWD_PREDICATE) ||
            (testValue000 == Logic.KWD_FUNCTION)) {
          result = Cons.cons(Symbol.internSymbolInModule(((Surrogate)(prop.operator)).symbolName, ((Module)(((Surrogate)(prop.operator)).homeContext)), true), result.reverse());
        }
        else if (testValue000 == Logic.KWD_EQUIVALENT) {
          result = Cons.cons(Logic.SYM_STELLA_e, result.reverse());
        }
        else if ((testValue000 == Logic.KWD_FORALL) ||
            (testValue000 == Logic.KWD_EXISTS)) {
          if (!(result.rest == Stella.NIL)) {
            result = Cons.consList(Cons.cons(Logic.SYM_STELLA_OR, Cons.cons(Cons.consList(Cons.cons(Logic.SYM_STELLA_NOT, Cons.cons(result.rest.value, Stella.NIL))), Cons.cons(result.value, Stella.NIL))));
          }
          else {
            result = ((Cons)(result.value));
          }
          { Cons bindings = Stella.NIL;

            { PatternVariable io = null;
              Vector vector001 = ((Vector)(KeyValueList.dynamicSlotValue(prop.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null)));
              int index001 = 0;
              int length001 = vector001.length();

              for (;index001 < length001; index001 = index001 + 1) {
                io = ((PatternVariable)((vector001.theArray)[index001]));
                if (Logic.argumentBoundTo(io) == null) {
                  bindings = Cons.cons(Cons.consList(Cons.cons(Symbol.internSymbol(Skolem.getSkolemPrintName(io)), Cons.cons(Symbol.internSymbol(Logic.logicalType(io).symbolName), Stella.NIL))), bindings);
                }
              }
            }
            if (!(bindings == Stella.NIL)) {
              result = Cons.consList(Cons.cons(Symbol.internSymbol(prop.kind.symbolName), Cons.cons(bindings, Cons.cons(result, Stella.NIL))));
            }
          }
        }
        else {
          result = Cons.cons(Symbol.internSymbol(((Surrogate)(prop.operator)).symbolName), result.reverse());
        }
      }
      if (Proposition.falseP(prop)) {
        return (Cons.list$(Cons.cons(Logic.SYM_STELLA_NOT, Cons.cons(result, Cons.cons(Stella.NIL, Stella.NIL)))));
      }
      else {
        return (result);
      }
    }
  }