proposition: Lemma Lam_bisimulation_4_1_5_lambda_star_bialgebra : forall (Lambda:T_over_B_distributive) (Xtb:TB_bialgebra) (hx:T_star_ (states Xtb.(coalgebra_part))), is_lambda_bialgebra Lambda Xtb -> lift_B_ _ _ (Beta_star Xtb) (lambda_star Lambda _ (lift_T_star_ _ _ (transition Xtb.(coalgebra_part)) hx)) = transition Xtb.(coalgebra_part) (Beta_star Xtb hx).
proof: Proof. intros Lambda [[X alpha_X] beta_X] hx hyp_lam_bialg. unfold Beta_star; simpl in *. set (tmp:=lift_T_star_ X (MB.F_ X) alpha_X hx). rewrite <- (Lam_bisimulation_4_1_5_lambda_star_universality Lambda (Build_F_algebra X beta_X)). simpl. subst tmp. rewrite (Lam_bisimulation_4_1_5_star_pres_algebra_morphism (Build_F_algebra X beta_X) (Build_F_algebra _ (fun tbx=>lift_B_ _ _ beta_X (lambda_ Lambda X tbx))) alpha_X); trivial. Qed.
imports: LambdaCoiteration