proposition: Lemma Beta_morphism : forall (Lambda: T_over_B_distributive) (tx ty: T_ w.(states)), (maximal_bisimulation (Build_F_coalgebra _ (fun s_bx=> Lambda.(lambda_) _ (lift_T_ _ _ (transition w) s_bx))) (Build_F_coalgebra _ (fun s_bx=> Lambda.(lambda_) _ (lift_T_ _ _ (transition w) s_bx))) tx ty) -> Beta Lambda tx (=) Beta Lambda ty.
proof: Proof. intros [lam_ nat_lam] tx ty hyp; unfold Beta; apply B_unfold_morphism; assumption. Qed.
imports: WeaklyFinalCoalgebra