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 Str_unique_with_cons; intros s; assert (Hfs:=Hf s);assert (Hgs:=Hg s); destruct S0 as [S0_st S0_tr]; simpl in f,g,Hf,Hg,s, Hfs, Hgs. rewrite (hd_tl_id (f s)); apply f_equal2; [ unfold hd_; change (fst (hd (f s), tl (f s))=fst (S0_tr s)) | unfold tl_; change (snd (hd (f s), tl (f s))=f (snd (S0_tr s))) ]; destruct (S0_tr s) as [h_s t_s]; rewrite Hfs; simpl; trivial. rewrite (hd_tl_id (g s)); apply f_equal2; [ unfold hd_; change (fst (hd (g s), tl (g s))=fst (S0_tr s)) | unfold tl_; change (snd (hd (g s), tl (g s))=g (snd (S0_tr s))) ]; destruct (S0_tr s) as [h_s t_s]; rewrite Hgs; simpl; trivial. Qed.
imports: WeaklyFinalCoalgebra