public static Cons kifForallToStellaForall(Cons tree) {
    if ((tree.length() < 3) ||
        (tree.length() > 4)) {
      { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

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

          try {
            Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
            stream000.nativeStream.println("PARSING ERROR: Illegal FORALL tree: `" + tree + "'.");
            Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

          } finally {
            Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
          }
        }
        throw ((ParsingError)(ParsingError.newParsingError(stream000.theStringReader()).fillInStackTrace()));
      }
    }
    { Cons declarations = Logic.kifVariableDeclarationsToStella(tree.rest.value, true);

      switch (tree.length()) {
        case 3: 
          return (Logic.kifTwoArgumentForallToStellaForall(tree, declarations));
        case 4: 
          return (Logic.kifThreeArgumentForallToStellaForall(tree, declarations));
        default:
          { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

            stream001.nativeStream.print("`" + tree.length() + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
          }
      }
    }
  }