public static void evaluateEquivalentProposition(Proposition self) {
    { Vector arguments = self.arguments;
      Stella_Object firstarg = Logic.innermostOf((arguments.theArray)[0]);
      Stella_Object secondarg = Logic.innermostOf((arguments.theArray)[1]);

      if (Proposition.trueP(self)) {
        if (Proposition.defaultTrueP(self)) {
          Stella.STANDARD_WARNING.nativeStream.println("Warning: INTERNAL ERROR: DON'T KNOW YET HOW TO EQUATE THINGS BY DEFAULT.");
        }
        { Cons firstargtypes = Logic.allAssertedTypes(firstarg);
          Cons secondargtypes = Logic.allAssertedTypes(secondarg);

          { NamedDescription type1 = null;
            Cons iter000 = firstargtypes;

            for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
              type1 = ((NamedDescription)(iter000.value));
              { boolean foundP000 = false;

                { NamedDescription type2 = null;
                  Cons iter001 = secondargtypes;

                  loop001 : for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
                    type2 = ((NamedDescription)(iter001.value));
                    if (Description.disjointTermsP(type1, type2)) {
                      foundP000 = true;
                      break loop001;
                    }
                  }
                }
                if (foundP000) {
                  Proposition.signalUnificationClash(self, firstarg, secondarg);
                }
              }
            }
          }
        }
        Proposition.equateValues(self, firstarg, secondarg);
      }
      else if (Stella_Object.eqlP(firstarg, secondarg)) {
        Proposition.assignTruthValue(self, Stella.TRUE_WRAPPER);
      }
      else if ((!Logic.skolemP(firstarg)) &&
          (!Logic.skolemP(secondarg))) {
        Proposition.assignTruthValue(self, Stella.FALSE_WRAPPER);
      }
    }
  }