proposition: Lemma Lam_bisimulation_4_1_5_star_pres_algebra_morphism :forall (Xa Ya:F_algebra) (f: Xa.(carrier) -> Ya.(carrier)), (forall tx, Ya.(operation) (lift_T_ _ _ f tx) = f (Xa.(operation) tx)) -> (forall hx, (star_algebra Ya) (lift_T_star_ _ _ f hx) = f ((star_algebra Xa) hx)).
proof: Proof. intros Xa Ya f hyp_alg_map [j tjx]. unfold star_algebra. simpl in *. apply (Lam_bisimulation_4_1_5_iterate_pres_algebra_morphism j); trivial. Qed.
imports: LambdaCoiteration