proposition: Lemma CoPeano_unfold_unfolded:forall (S0:F_coalgebra) (s0: S0.(states)), CoPeano_unfold S0 s0 = match S0.(transition) s0 with | inl star => co_O | inr x => co_S (CoPeano_unfold S0 x) end.
proof: Proof. intros S0 x. rewrite (unfold_conat (CoPeano_unfold S0 x)). destruct S0 as [X X_tr]. 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; rewrite <- hyp_X; reflexivity. Qed.
imports: WeaklyFinalCoalgebra