proposition: Theorem is_lambda_bisimulation_commute_span: 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) (hr:T_star_ {s1s2 : states (coalgebra_part Xtb) * states (coalgebra_part Ytb) |lR (fst s1s2) (snd s1s2)}), 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 let T_star_gamma := lift_T_star_ _ _ (proj1_sig gamma_) in let lambda_star_TR := lambda_star Lambda (T_ lR_crr) in let B_Chi_R := lift_B_ _ _ (Chi lR_crr) in let alpha_gamma := fun hr0 => B_Chi_R (lambda_star_TR (T_star_gamma hr0)) in lift_B_ _ _ h_x (alpha_gamma hr) = (transition Xtb.(coalgebra_part)) (h_x hr) /\ lift_B_ _ _ h_y (alpha_gamma hr) = (transition Ytb.(coalgebra_part)) (h_y hr).
proof: Proof. intros Lambda Xtb Ytb lR [gamma hyp_gamma] tr hyp_X_bialgb hyp_Y_bialg lR_crr h_x h_y T_star_gamma lambda_star_TR B_Chi_R alpha_gamma; split; [subst h_x | subst h_y]; apply (is_like_lambda_bismulation_T_star_span_bisimulation Lambda (Build_BT_coalgebroid lR_crr gamma)); trivial; red; simpl; intros s1s2h; destruct (hyp_gamma s1s2h) as [Hx Hy]; [ apply Hx | apply Hy]; assumption. Qed.
imports: LambdaCoiteration