 In the other direction, the idea is to turn a bisimulation into a graph itself, and then extract two decorations of it; by the uniqueness part of AFA these must coincide. Here is how this is done in a concrete example.   We saw above that  