The coq proofs are available below; is used either the excluded middle or a well-foundedness hypothesis over the reduction relation (instead of the non-divergence hypothesis).

Instructions: Download the sources. You can directly use the files in interactive mode or with coqide (no compilation is needed). The main result is in the file unique_sol_thm.v. Details are explained in the comments, and in the README.

The files are split as follows, and in the following order:
• rels.v
A few lemmas and definitions regarding relations; the definitions of diagrams is usefull to define bisimulations and bisimilarities
• LTS.v
Defines the notion of Labeled Transition System (with internal tau steps), and the usual definitions of weak transitions in such a LTS.
• bsim.v
Definition and properties of weak bisimulations, and weak bisimilarity. Most of the work is related to the transitivity of weak bisimilarity.
• operators.v
Definition of autonomous transitions, then of sets of operators; also includes some properties of functions, extensional equality of functions, and composition of functions.
• divergences.v
Definitions of the notions of reducts of an operator and divergence of the infinite unfolding of an operator.
• unique_sol_prop.v
The first lemma: if an operator 'protects its solutions', then it has a unique solution up to weak bisimilarity.
• termination.v
A few lemmas regarding termination, non divergence, well-foundedness.
• unique_solution_steps.v
The main part of the proof of the main theorem: we build a sequence of transitions and operators, and use non divergence to show it must terminate; if it does, that proves that the operator protects its solution.
• unique_solution_thm.v
Putting everything together: statement of the main theorem.

Some important definitions (particularly those used as hypothesis, if one wants to check) are in:
LTS, weak transitions (wtrans, wttrans, whtrans): LTS.v
(strong and weak) bisimulation and bisimilarity: bsim.v
extensional equality of functions, autonomous transitions, guardedness, set of operators, weak autonomous transitions (waut, wtaut, whaut): operators.v
reduct (comp_red) of an operator, divergence (comp_div and div) of an operator (of its infinite unfolding): divergences.v
unique solution, protects its solutions: unique_sol_prop.v
the tau reduction relation (red_tau and reduction_tau) are in termination.v (for red_tau) and in unique_solution_thm.v (for reduction_tau). they are based on subrevR in termination.v, itself using comp_red from divergences.v