public static String propositionHeadSortString(Proposition p) {
    if (p.kind == Logic.KWD_IMPLIES) {
      if (Stella_Object.isaP((p.arguments.theArray)[0], Logic.SGT_LOGIC_DESCRIPTION) &&
          Stella_Object.isaP((p.arguments.theArray)[1], Logic.SGT_LOGIC_DESCRIPTION)) {
        return ("FORALL");
      }
      else {
        return ("SUBSET-OF");
      }
    }
    else {
      return (p.operator.symbolName);
    }
  }