proposition: Theorem lambda_coinduction_strong: forall (Lambda:T_over_B_distributive) (slR: w.(states) -> w.(states) -> Set) (x y:w.(states)), slR x y -> is_lambda_bisimulation_strong (Build_TB_bialgebra w (Beta Lambda)) (Build_TB_bialgebra w (Beta Lambda)) slR -> x (=) y.
proof: Proof. intros Lambda slR x y hyp_slR hyp_lam_bisim. apply (lambda_coinduction_lambda_bialgebras_strong Lambda (Build_TB_bialgebra w (Beta Lambda)) (Build_TB_bialgebra w (Beta Lambda)) slR hyp_lam_bisim x y hyp_slR); apply weakly_final_lambda_bialgebra. Qed.
imports: LambdaCoiteration