public static Cons kifBiconditionalToTwoImplies(Cons tree) {
    if (tree.length() > 3) {
      { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

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

          try {
            Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
            stream000.nativeStream.println("PARSING ERROR: Too many arguments to <=>: `" + tree + "'.");
            Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

          } finally {
            Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
          }
        }
        throw ((ParsingError)(ParsingError.newParsingError(stream000.theStringReader()).fillInStackTrace()));
      }
    }
    { Cons copy = ((Cons)(Stella_Object.copyConsTree(tree)));
      Stella_Object arrow = tree.value;
      Symbol forwardarrow = Logic.SYM_STELLA_eg;
      Symbol backwardarrow = Logic.SYM_STELLA_le;

      { GeneralizedSymbol testValue000 = ((GeneralizedSymbol)(arrow));

        if (testValue000 == Logic.SYM_LOGIC_legg) {
          forwardarrow = Logic.SYM_LOGIC_egg;
        }
        else if (testValue000 == Logic.SYM_LOGIC_lleg) {
          backwardarrow = Logic.SYM_LOGIC_lle;
        }
        else if (testValue000 == Logic.SYM_LOGIC_llegg) {
          forwardarrow = Logic.SYM_LOGIC_egg;
          backwardarrow = Logic.SYM_LOGIC_lle;
        }
        else if (testValue000 == Logic.SYM_LOGIC_ltg) {
          forwardarrow = Logic.SYM_LOGIC_tg;
          backwardarrow = Logic.SYM_LOGIC_lt;
        }
        else if (testValue000 == Logic.SYM_LOGIC_ltgg) {
          forwardarrow = Logic.SYM_LOGIC_tgg;
          backwardarrow = Logic.SYM_LOGIC_lt;
        }
        else if (testValue000 == Logic.SYM_LOGIC_lltg) {
          forwardarrow = Logic.SYM_LOGIC_tg;
          backwardarrow = Logic.SYM_LOGIC_llt;
        }
        else if (testValue000 == Logic.SYM_LOGIC_lltgg) {
          forwardarrow = Logic.SYM_LOGIC_tgg;
          backwardarrow = Logic.SYM_LOGIC_llt;
        }
        else {
        }
      }
      copy.firstSetter(forwardarrow);
      tree.firstSetter(backwardarrow);
      return (Cons.list$(Cons.cons(Logic.SYM_STELLA_AND, Cons.cons(tree, Cons.cons(Cons.cons(copy, Stella.NIL), Stella.NIL)))));
    }
  }