proposition: Lemma F_coalgebra_compose:forall (S0 S1 S2:F_coalgebra) f g, (forall (s0: S0.(states)), S1.(transition) (f s0) = lift_F_ _ _ f (S0.(transition) s0)) -> (forall (s1: S1.(states)), S2.(transition) (g s1) = lift_F_ _ _ g (S1.(transition) s1)) -> forall s0, S2.(transition) (g (f s0)) = lift_F_ _ _ (fun s=>g (f s)) (S0.(transition) s0).
proof: Proof. intros [X0 X0_tr] [X1 X1_tr] [X2 X2_tr]; simpl; intros f g Hf Hg s0. rewrite (Hg (f s0)). rewrite (Hf s0). rewrite lift_F_compose; trivial. Qed.
imports: ExtensionalFunctor Setoid