proposition: Lemma CoPeano_unique_with_cons:forall (S0:F_coalgebra) f g, (forall (s0: S0.(states)), (f s0) = match S0.(transition) s0 with | inl star => co_O | inr x => co_S (f x) end) -> (forall (s0: S0.(states)), (g s0) = match S0.(transition) s0 with | inl star => co_O | inr x => co_S (g x) end) -> forall s, f s(=) g s.
proof: Proof. intros S0 f g Hf Hg s0. apply trans_bisimilar with (CoPeano_unfold S0 s0); [apply sym_bisimilar|]; apply CoPeano_unfold_bisim_unique ; assumption. Qed.
imports: WeaklyFinalCoalgebra