public static Cons helpBuildQuantifiedProposition(Cons tree, boolean converttypestoconstraintsP, Object [] MV_returnarray) {
    { Object old$Variabletypepropositions$000 = Logic.$VARIABLETYPEPROPOSITIONS$.get();

      try {
        Native.setSpecial(Logic.$VARIABLETYPEPROPOSITIONS$, Stella.NIL);
        { Stella_Object quantifier = tree.value;
          Stella_Object antecedentclause = tree.rest.rest.value;
          Stella_Object consequentclause = tree.fourth();
          Cons variables = null;
          Proposition antecedentproposition = null;
          Proposition consequentproposition = null;

          variables = Logic.parseLogicVariableDeclarations(tree.rest.value);
          if (antecedentclause != null) {
            antecedentproposition = ((Proposition)(Logic.buildProposition(antecedentclause)));
          }
          if (consequentclause != null) {
            consequentproposition = ((Proposition)(Logic.buildProposition(consequentclause)));
          }
          Logic.popLogicVariableBindings(variables);
          if (converttypestoconstraintsP) {
            if (!(((Cons)(Logic.$VARIABLETYPEPROPOSITIONS$.get())) == Stella.NIL)) {
              if (antecedentproposition != null) {
                Native.setSpecial(Logic.$VARIABLETYPEPROPOSITIONS$, Cons.cons(antecedentproposition, ((Cons)(Logic.$VARIABLETYPEPROPOSITIONS$.get()))));
              }
              Native.setSpecial(Logic.$VARIABLETYPEPROPOSITIONS$, ((Cons)(Logic.$VARIABLETYPEPROPOSITIONS$.get())).reverse().removeDuplicates());
              antecedentproposition = Logic.conjoinPropositions(((Cons)(Logic.$VARIABLETYPEPROPOSITIONS$.get())));
            }
          }
          { Cons _return_temp = variables;

            MV_returnarray[0] = antecedentproposition;
            MV_returnarray[1] = consequentproposition;
            return (_return_temp);
          }
        }

      } finally {
        Logic.$VARIABLETYPEPROPOSITIONS$.set(old$Variabletypepropositions$000);
      }
    }
  }