proposition: Lemma Lam_bisimulation_4_1_5_lambda_star_universality : forall (Lambda:T_over_B_distributive) (Xtb:F_algebra) (hbx:T_star_ (B_ Xtb.(carrier))), star_algebra (Build_F_algebra (B_ Xtb.(carrier)) (fun tbx => lift_B_ _ _ Xtb.(operation) (Lambda.(lambda_) _ tbx))) hbx = lift_B_ _ _ (star_algebra Xtb) (lambda_star Lambda _ hbx).
proof: Proof. intros Lambda Xtb [j tjbx]. simpl. rewrite lift_B_compose; fold lift_B_. unfold star_algebra. simpl. apply (Lam_bisimulation_4_1_5_lambda_star_iterate Lambda j Xtb tjbx). Qed.
imports: LambdaCoiteration