proposition: Lemma lambda_bisimulation_strong_included_image_span: forall (Lambda:T_over_B_distributive) (Xtb Ytb:TB_bialgebra) (slR: states (Xtb.(coalgebra_part)) -> states (Ytb.(coalgebra_part)) -> Set) (gamma_: is_lambda_bisimulation_strong _ _ slR) (x:states Xtb.(coalgebra_part)) (y:states Ytb.(coalgebra_part)), slR x y -> is_lambda_bialgebra Lambda Xtb -> is_lambda_bialgebra Lambda Ytb -> let slR_crr:= {s1s2 : states (coalgebra_part Xtb) * states (coalgebra_part Ytb) &slR (fst s1s2) (snd s1s2)} in let h_x := fun hr => (Beta_star Xtb) (lift_T_star_ _ _ (fun s1s2h:slR_crr => fst (projT1 s1s2h)) hr) in let h_y := fun hr => (Beta_star Ytb) (lift_T_star_ _ _ (fun s1s2h:slR_crr => snd (projT1 s1s2h)) hr) in {hr:T_star_ slR_crr | h_x hr = x /\ h_y hr= y} .
proof: Proof. intros Lambda Xtb Ytb slR gamma_ x y hyp_slR hyp_x_bialg hyp_y_bialg slR_crr h_x h_y. exists (T_star_coproject_ slR_crr O (existT (fun xy => slR (fst xy) (snd xy)) (x,y) hyp_slR)). subst h_x h_y; simpl in *; split; trivial. Qed.
imports: LambdaCoiteration