proposition: Theorem lambda_coinduction: forall (Lambda:T_over_B_distributive) (lR: w.(states) -> w.(states) -> Prop) (x y:w.(states)), lR x y -> is_lambda_bisimulation (Build_TB_bialgebra w (Beta Lambda)) (Build_TB_bialgebra w (Beta Lambda)) lR -> x (=) y.
proof: Proof. intros Lambda lR x y hyp_lR hyp_lam_bisim. apply (lambda_coinduction_lambda_bialgebras Lambda (Build_TB_bialgebra w (Beta Lambda)) (Build_TB_bialgebra w (Beta Lambda)) lR hyp_lam_bisim x y hyp_lR); apply weakly_final_lambda_bialgebra. Qed.
imports: LambdaCoiteration