proposition: Lemma Str_unique_with_cons:forall (S0:F_coalgebra) f g, (forall (s0: S0.(states)), (f s0) = Cons (hd_ S0 s0) (f (tl_ S0 s0))) -> (forall (s0: S0.(states)), (g s0) = Cons (hd_ S0 s0) (g (tl_ S0 s0))) -> forall s, f s(=) g s.
proof: Proof. intros S0 f g Hf Hg s0. apply trans_bisimilar with (Str_unfold S0 s0); [apply sym_bisimilar|]; apply Str_unfold_bisim_unique ; assumption. Qed.
imports: WeaklyFinalCoalgebra