public static void unifyTypes(Proposition prop, Skolem term1, Stella_Object term2) {
    { Surrogate type1 = Logic.logicalType(term1);
      Surrogate type2 = Logic.logicalType(term2);

      if ((type1 == type2) ||
          (Logic.logicalSubtypeOfP(type1, type2) ||
           Logic.logicalSubtypeOfP(type2, type1))) {
      }
      else if (type1 == Logic.SGT_STELLA_THING) {
        if (Stella_Object.isaP(term1, Logic.SGT_LOGIC_SKOLEM)) {
        }
        ((Skolem)(term1)).skolemType = type2;
      }
      else if (type2 == Logic.SGT_STELLA_THING) {
        if (Stella_Object.isaP(term2, Logic.SGT_LOGIC_SKOLEM)) {
          ((Skolem)(term2)).skolemType = type1;
        }
      }
      else {
        if (Logic.bottomP(term2)) {
          return;
        }
        Proposition.signalUnificationClash(prop, term1, term2);
      }
    }
  }