public static void normalizeForallProposition(Proposition self) {
    { Stella_Object antarg = (self.arguments.theArray)[0];
      Stella_Object cqarg = (self.arguments.theArray)[1];
      Proposition antecedent = null;
      Proposition consequent = null;

      if (Logic.variableP(antarg) ||
          Logic.variableP(cqarg)) {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          { Object old$PrintreadablyP$000 = Stella.$PRINTREADABLYp$.get();

            try {
              Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
              stream000.nativeStream.println("ERROR: Can't yet handle propositional variables within FORALL.");
              Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

            } finally {
              Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
            }
          }
          throw ((PropositionError)(PropositionError.newPropositionError(stream000.theStringReader()).fillInStackTrace()));
        }
      }
      antecedent = ((Proposition)(antarg));
      consequent = ((Proposition)(cqarg));
      { Object old$Evaluationmode$000 = Logic.$EVALUATIONMODE$.get();

        try {
          Native.setSpecial(Logic.$EVALUATIONMODE$, Logic.KWD_DESCRIPTION);
          Proposition.normalizeProposition(antecedent);
          Proposition.normalizeProposition(consequent);

        } finally {
          Logic.$EVALUATIONMODE$.set(old$Evaluationmode$000);
        }
      }
      if (antecedent.kind == Logic.KWD_CONSTANT) {
        { GeneralizedSymbol testValue000 = antecedent.operator;

          if (testValue000 == Logic.SGT_STELLA_TRUE) {
            if (Proposition.migrateConsequentGoalsToAntecedentP(self)) {
              return;
            }
          }
          else if (testValue000 == Logic.SGT_STELLA_FALSE) {
            Proposition.overlayWithConstantProposition(self, Logic.TRUE_PROPOSITION);
            return;
          }
          else {
            { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

              stream001.nativeStream.print("`" + testValue000 + "' is not a valid case option");
              throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
            }
          }
        }
      }
      { Keyword testValue001 = consequent.kind;

        if (testValue001 == Logic.KWD_FORALL) {
          if (!Logic.naturalDeductionModeP()) {
            Proposition.flattenNestedForallProposition(self);
          }
        }
        else if (testValue001 == Logic.KWD_CONSTANT) {
          { GeneralizedSymbol testValue002 = consequent.operator;

            if (testValue002 == Logic.SGT_STELLA_FALSE) {
              Proposition.overlayProposition(self, antecedent);
              Proposition.invertProposition(self);
              return;
            }
            else if (testValue002 == Logic.SGT_STELLA_TRUE) {
              Proposition.overlayWithConstantProposition(self, Logic.TRUE_PROPOSITION);
              return;
            }
            else {
              { OutputStringStream stream002 = OutputStringStream.newOutputStringStream();

                stream002.nativeStream.print("`" + testValue002 + "' is not a valid case option");
                throw ((StellaException)(StellaException.newStellaException(stream002.theStringReader()).fillInStackTrace()));
              }
            }
          }
        }
        else {
        }
      }
      if (((Vector)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))).emptyP()) {
        antecedent = Proposition.invertProposition(antecedent);
        Proposition.overlayProposition(self, Logic.disjoinPropositions(Cons.consList(Cons.cons(antecedent, Cons.cons(consequent, Stella.NIL)))));
        Proposition.normalizeProposition(self);
        return;
      }
      { Proposition impliesproposition = Proposition.deriveImpliesFromForall(self);

        if (impliesproposition != null) {
          Proposition.overlayProposition(self, impliesproposition);
        }
      }
    }
  }