public static void printKifQuantification(Proposition self) {
    { OutputStream stream = ((OutputStream)(Logic.$PRINTLOGICALFORMSTREAM$.get()));
      Proposition tail = ((Proposition)((self.arguments.theArray)[0]));
      Proposition head = ((self.arguments.length() == 2) ? ((Proposition)((self.arguments.theArray)[1])) : null);
      boolean implicationP = head != null;
      Surrogate implicationoperator = (implicationP ? Proposition.chooseImplicationOperator(self, ((BooleanWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue) : ((Surrogate)(null)));

      if ((implicationoperator != null) &&
          (((BooleanWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue &&
           (!(implicationoperator == Logic.SGT_PL_KERNEL_KB_le)))) {
        { Proposition temp = tail;

          tail = head;
          head = temp;
        }
      }
      { Keyword testValue000 = self.kind;

        if (testValue000 == Logic.KWD_FORALL) {
          stream.nativeStream.print("(" + Logic.stringifiedSurrogate(Logic.SGT_PL_KERNEL_KB_FORALL) + " ");
        }
        else if (testValue000 == Logic.KWD_EXISTS) {
          stream.nativeStream.print("(" + Logic.stringifiedSurrogate(Logic.SGT_PL_KERNEL_KB_EXISTS) + " ");
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
      Logic.printKifQuantifiedVariables(((Vector)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))), false);
      stream.nativeStream.println();
      Logic.increaseIndent(Stella.NULL_INTEGER);
      Logic.printIndent(stream, Stella.NULL_INTEGER);
      if (implicationP) {
        stream.nativeStream.print("(" + Logic.stringifiedSurrogate(implicationoperator) + " ");
        Logic.increaseIndent((implicationoperator.symbolName).length() + 2);
        Proposition.printKifProposition(head);
        stream.nativeStream.println();
        Logic.printIndent(stream, Stella.NULL_INTEGER);
      }
      Proposition.printKifProposition(tail);
      if (implicationP) {
        stream.nativeStream.print(")");
        Logic.decreaseIndent((implicationoperator.symbolName).length() + 2);
      }
      Logic.decreaseIndent(Stella.NULL_INTEGER);
      stream.nativeStream.print(")");
    }
  }