proposition: Theorem lambda_coinduction_lambda_bialgebras: 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) (x:states Xtb.(coalgebra_part)) (y:states Ytb.(coalgebra_part)), lR x y -> is_lambda_bialgebra Lambda Xtb -> is_lambda_bialgebra Lambda Ytb -> (maximal_bisimulation Xtb.(coalgebra_part) Ytb.(coalgebra_part) x y).
proof: Proof. intros Lambda Xtb Ytb lR gamma_ x y hyp_lR hyp_x_bialg hyp_y_bialg. destruct (maximal_bisimulation_is_maximal Xtb.(coalgebra_part) Ytb.(coalgebra_part)) as [_ hyp_max]. set (lR_crr:= {s1s2 : states (coalgebra_part Xtb) * states (coalgebra_part Ytb) |lR (fst s1s2) (snd s1s2)}). set (h_x := fun hr => (Beta_star Xtb) (lift_T_star_ _ _ (fun s1s2h:lR_crr => fst (proj1_sig s1s2h)) hr)). set (h_y := fun hr => (Beta_star Ytb) (lift_T_star_ _ _ (fun s1s2h:lR_crr => snd (proj1_sig s1s2h)) hr)). apply (hyp_max (fun x=>(fun y=>{hr:T_star_ lR_crr | h_x hr = x /\ h_y hr= y} ))). exists (is_lambda_bisimulation_F_bisimulation_strong Lambda Xtb Ytb lR gamma_ hyp_x_bialg hyp_y_bialg); trivial. apply (lambda_bisimulation_included_image_span Lambda Xtb Ytb lR gamma_ x y hyp_lR hyp_x_bialg hyp_y_bialg). Qed.
imports: LambdaCoiteration