public static Proposition buildForallProposition(Cons tree) {
    { Proposition forallprop = Logic.createProposition(Logic.SYM_STELLA_FORALL, 2);

      { Cons variables = null;
        Proposition antecedent = null;
        Proposition consequent = null;

        { Object [] caller_MV_returnarray = new Object[2];

          variables = Logic.buildQuantifiedProposition(tree, true, caller_MV_returnarray);
          antecedent = ((Proposition)(caller_MV_returnarray[0]));
          consequent = ((Proposition)(caller_MV_returnarray[1]));
        }
        forallprop.kind = Logic.KWD_FORALL;
        KeyValueList.setDynamicSlotValue(forallprop.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, Logic.copyConsListToVariablesVector(variables), null);
        (forallprop.arguments.theArray)[0] = (((antecedent != null) ? antecedent : Logic.TRUE_PROPOSITION));
        (forallprop.arguments.theArray)[1] = consequent;
      }
      return (forallprop);
    }
  }