public static Surrogate getPropositionBaseOperator(Proposition prop) {
    if (prop.kind == Logic.KWD_EQUIVALENT) {
      { Stella_Object term1 = (prop.arguments.theArray)[0];
        Stella_Object term2 = (prop.arguments.theArray)[1];

        if (Logic.functionOutputSkolemP(term1)) {
          return (((Surrogate)(((Skolem)(term1)).definingProposition.operator)));
        }
        else if (Logic.functionOutputSkolemP(term2)) {
          return (((Surrogate)(((Skolem)(term2)).definingProposition.operator)));
        }
        else {
          return (((Surrogate)(prop.operator)));
        }
      }
    }
    return (((Surrogate)(prop.operator)));
  }