proposition: Lemma ordinary_coinduction:forall (R: w.(states)-> w.(states)->Prop) x y, R x y-> is_F_bisimulation _ _ R -> x (=) y.
proof: Proof. intros R x y hyp_R hyp_bisim; apply bisimulation_maximal_bisimulation with R; trivial. Qed.
imports: Bisimulation