proposition: Lemma lambda_coinduction_lambda_bialgebras_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) -> forall r, (maximal_bisimulation Xtb.(coalgebra_part) Ytb.(coalgebra_part) (f r) (g r)).
proof: Proof. intros Lambda Rbt Xtb Ytb f g hyp_x_bialg hyp_y_bialg hyp_f hyp_g r. destruct (maximal_bisimulation_is_maximal Xtb.(coalgebra_part) Ytb.(coalgebra_part)) as [_ hyp_max]. set (h_f := fun hr => (Beta_star Xtb) (lift_T_star_ _ _ f hr)). set (h_g := fun hr => (Beta_star Ytb) (lift_T_star_ _ _ g hr)). apply (hyp_max (fun x=>(fun y=>{hr:T_star_ Rbt.(bs_states) | h_f hr = x /\ h_g hr = y} ))). exists (is_lambda_bisimulation_F_bisimulation_strong_like Lambda Rbt Xtb Ytb f g hyp_x_bialg hyp_y_bialg hyp_f hyp_g); trivial. apply (lambda_bisimulation_included_image_span_like Lambda Rbt Xtb Ytb f g hyp_x_bialg hyp_y_bialg hyp_f hyp_g). Qed.
imports: LambdaCoiteration