public static Proposition expandIfProposition(Proposition ifproposition) {
    { Vector arguments = ifproposition.arguments;
      Stella_Object testprop = (arguments.theArray)[0];
      Proposition negatedtestprop = Logic.createProposition(Logic.SYM_STELLA_NOT, 1);
      Stella_Object truevalue = (arguments.theArray)[1];
      Stella_Object falsevalue = (arguments.theArray)[2];
      PatternVariable valuevariable = ((PatternVariable)((ifproposition.arguments.theArray)[(ifproposition.arguments.length() - 1)]));
      Proposition trueequivalence = Logic.createEquivalenceProposition(valuevariable, truevalue);
      Proposition falseequivalence = ((falsevalue != null) ? Logic.createEquivalenceProposition(valuevariable, falsevalue) : ((Proposition)(null)));

      valuevariable.definingProposition = null;
      if (falsevalue != null) {
        {
          (negatedtestprop.arguments.theArray)[0] = ((Stella_Object.isaP(testprop, Logic.SGT_LOGIC_PATTERN_VARIABLE) ? testprop : Proposition.shallowCopyProposition(((Proposition)(testprop)))));
          return (Logic.disjoinPropositions(Cons.consList(Cons.cons(Proposition.conjoinTwoPropositions(((Proposition)(testprop)), trueequivalence), Cons.cons(Proposition.conjoinTwoPropositions(negatedtestprop, falseequivalence), Stella.NIL)))));
        }
      }
      else {
        return (Proposition.conjoinTwoPropositions(((Proposition)(testprop)), trueequivalence));
      }
    }
  }