proposition: Lemma commutativity_Str_unfold (S0: F_coalgebra) (x:S0.(states)) : Str.(transition) (Str_unfold S0 x) = (lift_F_ _ _ (Str_unfold S0)) (S0.(transition) x).
proof: Proof. destruct S0 as [s0 s0_tr]. rewrite Str_unfold_unfolded; simpl. set (s0_tr_x:=s0_tr x). destruct s0_tr_x as (b,tr); trivial. Qed.
imports: WeaklyFinalCoalgebra