public static Proposition updateEquivalenceProposition(Proposition proposition, Keyword updatemode) {
    { Stella_Object term1 = (proposition.arguments.theArray)[0];
      Stella_Object term2 = (proposition.arguments.theArray)[1];

      if (Logic.skolemP(term1) &&
          Logic.skolemP(term2)) {
        if (updatemode == Logic.KWD_PRESUME_TRUE) {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

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

              try {
                Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
                {
                  stream000.nativeStream.println("ERROR: Equating two skolems by default is not yet supported.");
                  stream000.nativeStream.println(".");
                }
;
                Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

              } finally {
                Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
              }
            }
            throw ((PropositionError)(PropositionError.newPropositionError(stream000.theStringReader()).fillInStackTrace()));
          }
        }
        return (proposition);
      }
      if ((updatemode == Logic.KWD_ASSERT_TRUE) ||
          (updatemode == Logic.KWD_PRESUME_TRUE)) {
        Proposition.updatePropositionTruthValue(proposition, updatemode);
        if (Logic.clipValueP(term1, term2)) {
        }
        else if (Logic.clipValueP(term2, term1)) {
        }
        else {
          Proposition.equateValues(proposition, Logic.valueOf(term1), Logic.valueOf(term2));
        }
      }
      else if (updatemode == Logic.KWD_RETRACT_TRUE) {
        if (Logic.unequateValuesP(term1, term2)) {
        }
        else if (Logic.unequateValuesP(term2, term1)) {
        }
      }
      else if (updatemode == Logic.KWD_CONCEIVE) {
        return (proposition);
      }
      else {
        { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

          stream001.nativeStream.print("`" + updatemode + "' is not a valid case option");
          throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
        }
      }
      if (Logic.functionOutputSkolemP(term1) &&
          (!Logic.functionOutputSkolemP(term2))) {
        Proposition.runUpdatePropositionDemon(proposition, updatemode);
        return ((proposition.deletedP() ? null : ((Skolem)(term1)).definingProposition));
      }
      if (Logic.functionOutputSkolemP(term2) &&
          (!Logic.functionOutputSkolemP(term1))) {
        Proposition.runUpdatePropositionDemon(proposition, updatemode);
        return ((proposition.deletedP() ? null : ((Skolem)(term2)).definingProposition));
      }
      return (null);
    }
  }