proposition: Lemma is_like_lambda_bismulation_T_star_span_bisimulation (Lambda:T_over_B_distributive) (X:BT_coalgebroid) (Y:TB_bialgebra) (pi:X.(bs_states)->states Y.(coalgebra_part)) (hyp_lam_bisim:forall (r:X.(bs_states)), is_like_lambda_bismulation X Y pi r) (hr: T_star_ X.(bs_states)) : let P:=states Y.(coalgebra_part) in let alpha_P:=transition Y.(coalgebra_part) in let beta_P:=Y.(algebra_part) in let R:=X.(bs_states) in let gamma := X.(bs_transition) in let T_star_gamma := lift_T_star_ _ _ gamma in let lambda_star_TR := lambda_star Lambda (T_ R) in let B_Chi_R := lift_B_ _ _ (Chi R) in let alpha_gamma := fun hr0 => B_Chi_R (lambda_star_TR (T_star_gamma hr0)) in is_lambda_bialgebra Lambda Y -> lift_B_ _ _ (fun hr0=>Beta_star Y (lift_T_star_ _ _ pi hr0)) (alpha_gamma hr) = alpha_P (Beta_star Y (lift_T_star_ _ _ pi hr)).
proof: Proof. intros P alpha_P beta_P R gamma T_star_gamma lambda_star_TR B_Chi_R alpha_gamma hyp_lam_bialg. red in hyp_lam_bisim. fold P R lift_B_. rewrite <- (lift_B_compose _ _ _ (lift_T_star_ R P pi) (Beta_star Y)). fold B_; fold lift_B_. unfold alpha_gamma. assert (square1: lift_B_ _ _ (lift_T_star_ R P pi) (B_Chi_R (lambda_star_TR (T_star_gamma hr))) = lift_B_ _ _ (Chi P) (lift_B_ _ _ (lift_T_star_ _ _ (lift_T_ R P pi)) (lambda_star_TR (T_star_gamma hr)))). unfold B_Chi_R; do 2 rewrite lift_B_compose; fold lift_B_; apply lift_B_extensionality; intros [j tx_]; trivial. rewrite square1. set (tmp:=(lift_B_ _ _ (lift_T_star_ _ _ (lift_T_ R P pi)) (lambda_star_TR (T_star_gamma hr)))). assert (square2: lift_B_ _ _ (Beta_star Y) (lift_B_ _ _ (Chi P) tmp) = lift_B_ _ _ (Beta_star Y) (lift_B_ _ _ (lift_T_star_ _ _ beta_P) tmp) ). simpl; do 2 rewrite lift_B_compose; fold lift_B_; apply lift_B_extensionality; intros [j ttx]; trivial. fold P in square2;fold P; unfold carrier in *; rewrite square2. subst tmp. rewrite (lift_B_compose _ _ _ (lift_T_star_ (F_ R) (F_ P) (lift_T_ R P pi)) (lift_T_star_ (F_ P) P beta_P)). fold lift_B_. assert (foo:=lift_T_star_compose _ _ _ (lift_T_ R P pi) beta_P). fold P in foo. stepl (lift_B_ _ _ (Beta_star Y) (lift_B_ _ _ (lift_T_star_ _ _ (fun x => beta_P (lift_T_ R P pi x))) (lambda_star_TR (T_star_gamma hr))) ); [ |do 2 rewrite lift_B_compose; fold lift_B_; apply lift_B_extensionality; intros; f_equal; rewrite lift_T_star_compose; trivial]. set (tmp:=T_star_gamma hr). assert (square3: lift_B_ (T_star_ (F_ R)) (T_star_ (states (coalgebra_part Y))) (lift_T_star_ (F_ R) (states (coalgebra_part Y)) (fun x : F_ R => beta_P (lift_T_ R P pi x))) (lambda_star_TR tmp) =lambda_star Lambda P (lift_T_star_ _ _ (lift_B_ _ _ (fun x : F_ R => beta_P (lift_T_ R P pi x))) tmp)). generalize tmp as tsbx. apply lambda_star_naturality. rewrite square3. fold B_ T_ P. subst tmp. stepl (lift_B_ _ _ (Beta_star Y) (lambda_star Lambda P (lift_T_star_ _ _ alpha_P (lift_T_star_ _ _ pi hr)) )); [ | do 2 f_equal; unfold T_star_gamma, alpha_P; do 2 rewrite lift_T_star_compose; fold R P B_; apply lift_T_star_extensionality; intros r; symmetry; fold R P B_ T_ gamma in hyp_lam_bisim; apply hyp_lam_bisim ]. fold P R. set (tmp:=lift_T_star_ R P pi hr). apply Lam_bisimulation_4_1_5_lambda_star_bialgebra. intros tx. generalize(Lam_bisimulation_4_1_5_lambda_star_bialgebra Lambda Y). intros H_lambda_star. apply hyp_lam_bialg. Qed.
imports: LambdaCoiteration