proposition: Lemma Str_unfold_bisim_unique:forall (S0:F_coalgebra) f, (forall (s0: S0.(states)), (f s0) = Cons (hd_ S0 s0) (f (tl_ S0 s0))) -> forall s, Str_unfold S0 s(=) f s.
proof: Proof. cofix. intros S0 f H s0. rewrite Str_unfold_unfolded. rewrite (H s0). constructor; trivial. simpl. apply (Str_unfold_bisim_unique _ _ H (tl_ S0 s0)). Qed.
imports: WeaklyFinalCoalgebra