proposition: Lemma commutativity_CoPeano_unfold (S0: F_coalgebra) (x:S0.(states)) : CoPeano.(transition) (CoPeano_unfold S0 x) = (lift_F_ _ _ (CoPeano_unfold S0)) (S0.(transition) x).
proof: Proof. destruct S0 as [X X_tr]. unfold lift_F_; simpl. set (X_tr_x:=X_tr x). destruct X_tr_x as [u|x']; trivial. destruct u; reflexivity. Qed.
imports: WeaklyFinalCoalgebra