proposition: Lemma lambda_bisimulation_included_image_span_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 forall r, {hr : T_star_ (bs_states Rbt) | h_f hr = f r /\ h_g hr = g r}.
proof: Proof. intros Lambda Rbt Xtb Ytb f g hyp_x_bialg hyp_y_bialg hyp_f hyp_g h_f h_g r. exists (T_star_coproject_ Rbt.(bs_states) O r). subst h_f h_g; simpl in *; split; trivial. Qed.
imports: LambdaCoiteration