proposition: Lemma Beta_corecursor_cotupling_id: forall (x: T_ w.(states)), Beta prim_corec_distributive x (=) prim_corec_tupling _ (fun x0 => x0) x.
proof: Proof. apply (F_unique (Build_F_coalgebra _ (fun s_bx=> lambda_corecursion _ (lift_T_ _ _ (transition w) s_bx)))). intros x; apply (commutativity_F_unfold _ x). intros [x0 | w0]; simpl; rewrite lift_B_compose; apply lift_B_id. Qed.
imports: WeaklyFinalCoalgebra