proposition: Theorem is_lambda_bisimulation_F_bisimulation_strong: forall (Lambda:T_over_B_distributive) (Xtb Ytb:TB_bialgebra) (lR: states (Xtb.(coalgebra_part)) -> states (Ytb.(coalgebra_part)) -> Prop) (gamma_: is_lambda_bisimulation _ _ lR) , is_lambda_bialgebra Lambda Xtb -> is_lambda_bialgebra Lambda Ytb -> let lR_crr:= {s1s2 : states (coalgebra_part Xtb) * states (coalgebra_part Ytb) |lR (fst s1s2) (snd s1s2)} in let h_x := fun hr => (Beta_star Xtb) (lift_T_star_ _ _ (fun s1s2h:lR_crr => fst (proj1_sig s1s2h)) hr) in let h_y := fun hr => (Beta_star Ytb) (lift_T_star_ _ _ (fun s1s2h:lR_crr => snd (proj1_sig s1s2h)) hr) in is_F_bisimulation_strong Xtb.(coalgebra_part) Ytb.(coalgebra_part) (fun x=>(fun y=>{hr:T_star_ lR_crr | h_x hr = x /\ h_y hr= y} )).
proof: Proof. intros Lambda Xtb Ytb lR gamma_ hyp_x_bialg hyp_y_bialg lR_crr h_x h_y. set (T_star_gamma := lift_T_star_ _ _ (proj1_sig gamma_)). set (lambda_star_TR := lambda_star Lambda (T_ lR_crr)). set (B_Chi_R := lift_B_ _ _ (Chi lR_crr)). set (alpha_gamma := ( fun hr0 => B_Chi_R (lambda_star_TR (T_star_gamma hr0)) ): T_star_ lR_crr -> B_ (T_star_ lR_crr)). apply (image_span_is_F_bisimulation_strong Xtb.(coalgebra_part) (Build_F_coalgebra (T_star_ lR_crr) alpha_gamma) Ytb.(coalgebra_part)); intros s2; destruct (is_lambda_bisimulation_commute_span Lambda Xtb Ytb lR gamma_ s2 hyp_x_bialg hyp_y_bialg) as [hypl hypr]; simpl in *. apply hypl. apply hypr. Qed.
imports: LambdaCoiteration