public static Stella_Object wrapKifWithForall(Stella_Object tree, Cons declaredvariables) {
    if (Stella_Object.safePrimaryType(tree) == Logic.SGT_STELLA_CONS) {
      { Cons tree000 = ((Cons)(tree));

        if (Stella_Object.symbolP(tree000.value)) {
          { GeneralizedSymbol testValue000 = ((GeneralizedSymbol)(tree000.value));

            if (testValue000 == Logic.SYM_STELLA_AND) {
              { Cons sentences = Stella.NIL;

                { Stella_Object conjunct = null;
                  Cons iter000 = tree000.rest;
                  Cons collect000 = null;

                  for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
                    conjunct = iter000.value;
                    if (collect000 == null) {
                      {
                        collect000 = Cons.cons(Logic.wrapKifWithForall(conjunct, declaredvariables), Stella.NIL);
                        if (sentences == Stella.NIL) {
                          sentences = collect000;
                        }
                        else {
                          Cons.addConsToEndOfConsList(sentences, collect000);
                        }
                      }
                    }
                    else {
                      {
                        collect000.rest = Cons.cons(Logic.wrapKifWithForall(conjunct, declaredvariables), Stella.NIL);
                        collect000 = collect000.rest;
                      }
                    }
                  }
                }
                return (Cons.cons(Logic.SYM_STELLA_AND, sentences.concatenate(Stella.NIL, Stella.NIL)));
              }
            }
            else if (testValue000 == Logic.SYM_LOGIC_leg) {
              return (Logic.wrapKifWithForall(Logic.kifBiconditionalToTwoImplies(tree000), declaredvariables));
            }
            else {
            }
          }
        }
      }
    }
    else {
    }
    { List undeclaredvariables = List.newList();

      Logic.collectUndeclaredVariables(tree, declaredvariables, undeclaredvariables);
      switch (undeclaredvariables.length()) {
        case 0: 
          undeclaredvariables.free();
          return (tree);
        case 1: 
          return (Cons.list$(Cons.cons(Logic.SYM_STELLA_FORALL, Cons.cons(undeclaredvariables.first(), Cons.cons(Cons.cons(tree, Stella.NIL), Stella.NIL)))));
        default:
          return (Cons.list$(Cons.cons(Logic.SYM_STELLA_FORALL, Cons.cons(Stella_Object.copyConsTree(undeclaredvariables.theConsList), Cons.cons(Cons.cons(tree, Stella.NIL), Stella.NIL)))));
      }
    }
  }