proposition: Lemma is_lambda_bisimulation_F_bisimulation_strong_like: forall (Lambda:T_over_B_distributive) (Rbt:BT_coalgebroid) (Xtb Ytb:TB_bialgebra) (f: Rbt.(bs_states) -> states Xtb.(coalgebra_part)) (g: Rbt.(bs_states) -> states Ytb.(coalgebra_part)), is_lambda_bialgebra Lambda Xtb -> is_lambda_bialgebra Lambda Ytb -> (forall rtb, is_like_lambda_bismulation Rbt Xtb f rtb) -> (forall rtb, is_like_lambda_bismulation Rbt Ytb g rtb) -> let h_f := fun hr => (Beta_star Xtb) (lift_T_star_ _ _ f hr) in let h_g := fun hr => (Beta_star Ytb) (lift_T_star_ _ _ g hr) in is_F_bisimulation_strong Xtb.(coalgebra_part) Ytb.(coalgebra_part) (fun x=>(fun y=>{hr : T_star_ Rbt.(bs_states)| h_f hr = x /\ h_g hr = y})).
proof: Proof. intros Lambda Rbt Xtb Ytb f g hyp_x_bialg hyp_y_bialg hyp_f hyp_g h_f h_g. set (T_star_gamma := lift_T_star_ _ _ Rbt.(bs_transition)). set (lambda_star_TR := lambda_star Lambda (T_ Rbt.(bs_states))). set (B_Chi_R := lift_B_ _ _ (Chi Rbt.(bs_states))). set (alpha_gamma := ( fun hr0 => B_Chi_R (lambda_star_TR (T_star_gamma hr0)) ): T_star_ Rbt.(bs_states) -> B_ (T_star_ Rbt.(bs_states))). apply (image_span_is_F_bisimulation_strong Xtb.(coalgebra_part) (Build_F_coalgebra (T_star_ Rbt.(bs_states)) alpha_gamma) Ytb.(coalgebra_part)); intros s2. subst h_f; apply is_like_lambda_bismulation_T_star_span_bisimulation; trivial. subst h_g; apply is_like_lambda_bismulation_T_star_span_bisimulation; trivial. Qed.
imports: LambdaCoiteration