proposition: Lemma CoPeano_unfold_bisim_unique:forall (S0:F_coalgebra) f, (forall (s0: S0.(states)), f s0 = match S0.(transition) s0 with | inl star => co_O | inr x => co_S (f x) end) -> forall s, CoPeano_unfold S0 s(=) f s.
proof: Proof. cofix. intros [X X_tr] f hyp x. rewrite (hyp x). unfold transition. remember (X_tr x) as X_tr_x; revert HeqX_tr_x; pattern (X_tr_x); destruct (X_tr_x) as [u | x']; intros hyp_X;simpl. constructor 1; trivial; simpl; rewrite <- hyp_X; trivial. constructor 2 with (CoPeano_unfold (Build_F_coalgebra X X_tr) x') (f x'); simpl; [ rewrite <- hyp_X; reflexivity | reflexivity | apply (CoPeano_unfold_bisim_unique _ _ hyp)]. Qed.
imports: WeaklyFinalCoalgebra