proposition: Lemma F_unique:forall (S0:F_coalgebra) f g, (forall (s0: S0.(states)), w.(transition) (f s0) = (lift_F_ _ _ f) (S0.(transition) s0) ) -> (forall (s0: S0.(states)), w.(transition) (g s0) = (lift_F_ _ _ g) (S0.(transition) s0) ) -> forall s, f s(=) g s.
proof: Proof. intros S0 f g; simpl; unfold lift_F_; intros Hf Hg. apply CoPeano_unique_with_cons; intros s; assert (Hfs:=Hf s);assert (Hgs:=Hg s); destruct S0 as [S0_st S0_tr]; simpl in *; [ destruct (S0_tr s) as [u|x']; [ apply pred_inl_co_O with u| apply pred_inr_co_S] | destruct (S0_tr s) as [u|x']; [ apply pred_inl_co_O with u| apply pred_inr_co_S] ]; symmetry; trivial. Qed.
imports: WeaklyFinalCoalgebra